Theory Lib
theory Lib
imports
Ordinary_Differential_Equations.ODE_Analysis
begin
section ‹Generic Mathematical Lemmas›
text‹General lemmas that don't have anything to do with dL specifically and could be fit for
general-purpose libraries, mostly dealing with derivatives, ODEs and vectors.›
lemma vec_extensionality:"(⋀i. v$i = w$i) ⟹ (v = w)"
by (simp add: vec_eq_iff)
lemma norm_axis: "norm (axis i x) = norm x"
unfolding axis_def norm_vec_def
unfolding L2_set_def
by(clarsimp simp add: if_distrib[where f=norm] if_distrib[where f="λx. x⇧2"] sum.If_cases)
lemma bounded_linear_axis: "bounded_linear (axis i)"
proof
show "axis i (x + y) = axis i x + axis i y" "axis i (r *⇩R x) = r *⇩R axis i x" for x y :: "'a" and r
by (auto simp: vec_eq_iff axis_def)
show "∃K. ∀x::'a. norm (axis i x) ≤ norm x * K"
by (auto simp add: norm_axis intro!: exI[of _ 1])
qed
lemma bounded_linear_vec:
fixes f::"('a::finite) ⇒ 'b::real_normed_vector ⇒ 'c::real_normed_vector"
assumes bounds:"⋀i. bounded_linear (f i)"
shows "bounded_linear (λx. χ i. f i x)"
proof unfold_locales
fix r x y
interpret bounded_linear "f i" for i by fact
show "(χ i. f i (x + y)) = (χ i. f i x) + (χ i. f i y)"
by (vector add)
show "(χ i. f i (r *⇩R x)) = r *⇩R (χ i. f i x)"
by (vector scaleR)
obtain K where "norm (f i x) ≤ norm x * K i" for x i
using bounded by metis
then have "norm (χ i. f i x) ≤ norm x * (∑i∈UNIV. K i)" (is "?lhs ≤ ?rhs") for x
unfolding sum_distrib_left
unfolding norm_vec_def
by (auto intro!: L2_set_le_sum_abs[THEN order_trans] sum_mono simp: abs_mult)
then show "∃K. ∀x. norm (χ i. f i x) ≤ norm x * K"
by blast
qed
lift_definition blinfun_vec::"('a::finite ⇒ 'b::real_normed_vector ⇒⇩L real) ⇒ 'b ⇒⇩L (real ^ 'a)" is "(λ(f::('a ⇒ 'b ⇒ real)) (x::'b). χ (i::'a). f i x)"
by(rule bounded_linear_vec, simp)
lemmas blinfun_vec_simps[simp] = blinfun_vec.rep_eq
lemma continuous_blinfun_vec:"(⋀i. continuous_on UNIV (blinfun_apply (g i))) ⟹ continuous_on UNIV (blinfun_vec g)"
by (simp add: continuous_on_vec_lambda)
lemma blinfun_elim:"⋀g. (blinfun_apply (blinfun_vec g)) = (λx. χ i. g i x)"
using blinfun_vec.rep_eq by auto
lemma sup_plus:
fixes f g::"('b::metric_space) ⇒ real"
assumes nonempty:"R ≠ {}"
assumes bddf:"bdd_above (f ` R)"
assumes bddg:"bdd_above (g ` R)"
shows "(SUP x∈R. f x + g x) ≤ (SUP x∈R. f x) + (SUP x∈R. g x)"
proof -
have bddfg:"bdd_above((λx. f x + g x ) ` R)"
using bddf bddg apply (auto simp add: bdd_above_def)
using add_mono_thms_linordered_semiring(1) by blast
have eq:"(SUP x∈R. f x + g x) ≤ (SUP x∈R. f x) + (SUP x∈R. g x)
⟷ (∀x∈R. (f x + g x) ≤ (SUP x∈R. f x) + (SUP x∈R. g x))"
apply(rule cSUP_le_iff)
subgoal by (rule nonempty)
subgoal by (rule bddfg)
done
have fs:"⋀x. x ∈ R ⟹ f x ≤ (SUP x∈R. f x)"
using bddf
by (simp add: cSUP_upper)
have gs:"⋀x. x ∈ R ⟹ g x ≤ (SUP x∈R. g x)"
using bddg
by (simp add: cSUP_upper)
have "(∀x∈R. (f x + g x) ≤ (SUP x∈R. f x) + (SUP x∈R. g x))"
apply auto
subgoal for x using fs[of x] gs[of x] by auto
done
then show ?thesis by (auto simp add: eq)
qed
lemma continuous_blinfun_vec':
fixes f::"'a::{finite,linorder} ⇒ 'b::{metric_space, real_normed_vector,abs} ⇒ 'b ⇒⇩L real"
fixes S::"'b set"
assumes conts:"⋀i. continuous_on UNIV (f i)"
shows "continuous_on UNIV (λx. blinfun_vec (λ i. f i x))"
proof (auto simp add: LIM_def continuous_on_def)
fix x1 and ε::real
assume ε:"0 < ε"
let ?n = "card (UNIV::'a set)"
have conts':" ⋀i x1 ε. 0 < ε ⟹ ∃δ>0. ∀x2. x2 ≠ x1 ∧ dist x2 x1 < δ ⟶ dist (f i x2) (f i x1) < ε"
using conts by(auto simp add: LIM_def continuous_on_def)
have conts'':"⋀i. ∃δ>0. ∀x2. x2 ≠ x1 ∧ dist x2 x1 < δ ⟶ dist (f i x2) (f i x1) < (ε/?n)"
subgoal for i using conts'[of "ε / ?n" x1 i] ε by auto done
let ?f = "(λx. blinfun_vec (λ i. f i x))"
let ?Pδ = "(λ i δ. (δ>0 ∧ (∀x2. x2 ≠ x1 ∧ dist x2 x1 < δ ⟶ dist (f i x2) (f i x1) < (ε/?n))))"
let ?δi = "(λi. SOME δ. ?Pδ i δ)"
have Ps:"⋀i. ∃δ. ?Pδ i δ" using conts'' by auto
have Pδi:"⋀i. ?Pδ i (?δi i)"
subgoal for i using someI[of "?Pδ i" ] Ps[of i] by auto done
have finU:"finite (UNIV::'a set)" by auto
let ?δ = "linorder_class.Min (?δi ` UNIV)"
have δ0s:"⋀i. ?δi i > 0" using Pδi by blast
then have δ0s':"⋀i. 0 < ?δi i" by auto
have bounds:"bdd_below (?δi ` UNIV)"
unfolding bdd_below_def
using δ0s less_eq_real_def by blast
have δs:"⋀i. ?δ ≤ ?δi i"
using bounds cINF_lower[of ?δi] by auto
have finite:"finite ((?δi ` UNIV))" by auto
have nonempty:"((?δi ` UNIV)) ≠ {}" by auto
have δ:"?δ > 0 " using Min_gr_iff[OF finite nonempty] δ0s'
by blast
have conts''':"⋀i x2. x2 ≠ x1 ⟹ dist x2 x1 < ?δi i ⟹ dist (f i x2) (f i x1) < (ε/?n)"
subgoal for i x2
using conts''[of i] apply auto
subgoal for δ
apply(erule allE[where x=x2])
using Pδi δs[of i] apply (auto simp add: δs[of i])
done
done
done
have "⋀x2. x2 ≠ x1 ∧ dist x2 x1 < ?δ ⟹ dist (blinfun_vec (λi. f i x2)) (blinfun_vec (λi. f i x1)) < ε"
proof (auto)
fix x2
assume ne:"x2 ≠ x1"
assume dist:"∀i. dist x2 x1 < ?δi i"
have dists:"⋀i. dist x2 x1 < ?δi i"
subgoal for i using dist δs[of i] by auto done
have euclid:"⋀y. norm(?f x1 y - ?f x2 y) = (L2_set (λi. norm(f i x1 y - f i x2 y)) UNIV)"
by (simp add: norm_vec_def)
have finite:"finite (UNIV::'a set)" by auto
have nonempty: "(UNIV::'a set) ≠ {}" by auto
have nonemptyB: "(UNIV::'b set) ≠ {}" by auto
have nonemptyR: "(UNIV::real set) ≠ {}" by auto
have SUP_leq:"⋀f::('b ⇒ real). ⋀ g::('b ⇒ real). ⋀ S::'b set. S ≠ {} ⟹ bdd_above (g ` S) ⟹ (⋀x. x ∈ (S::'b set) ⟹ ((f x)::real) ≤ ((g x)::real)) ⟹ (SUP x∈S. f x) ≤ (SUP x∈S. g x)"
by(rule cSup_mono, auto)
have SUP_sum_comm':"⋀R S f . finite (S::'a set) ⟹ (R::'d::metric_space set) ≠ {} ⟹
(⋀i x. ((f i x)::real) ≥ 0) ⟹
(⋀i. bdd_above (f i ` R)) ⟹
(SUP x∈R . (∑i ∈ S. f i x)) ≤ (∑i ∈ S. (SUP x∈R. f i x))"
proof -
fix R::"'d set" and S ::"('a)set" and f ::"'a ⇒ 'd ⇒ real"
assume non:"R ≠ {} "
assume fin:"finite S"
assume every:"(⋀i x. 0 ≤ f i x)"
assume bddF:"⋀i. bdd_above (f i ` R)"
then have bddF':"⋀i. ∃M. ∀x ∈R. f i x ≤ M "
unfolding bdd_above_def by auto
let ?boundP = "(λi M. ∀x ∈R. f i x ≤ M)"
let ?bound = "(λi::'a. SOME M. ∀x ∈R. f i x ≤ M)"
have "⋀i. ∃M. ?boundP i M" using bddF' by auto
then have each_bound:"⋀i. ?boundP i (?bound i)"
subgoal for i using someI[of "?boundP i"] by blast done
let ?bigBound = "(λF. ∑i∈F. (?bound i))"
have bddG:"⋀i::'a. ⋀F. bdd_above ((λx. ∑i∈F. f i x) ` R)"
subgoal for i F
using bddF[of i] unfolding bdd_above_def apply auto
apply(rule exI[where x="?bigBound F"])
subgoal for M
apply auto
subgoal for x
using each_bound by (simp add: sum_mono)
done
done
done
show "?thesis R S f" using fin assms
proof (induct)
case empty
have "((SUP x∈R. ∑i∈{}. f i x)::real) ≤ (∑i∈{}. SUP a∈R. f i a)" by (simp add: non)
then show ?case by auto
next
case (insert x F)
have "((SUP xa∈R. ∑i∈insert x F. f i xa)::real) ≤ (SUP xa∈R. f x xa + (∑i∈F. f i xa))"
using insert.hyps(2) by auto
moreover have "... ≤ (SUP xa∈ R. f x xa) + (SUP xa∈R. (∑i∈F. f i xa))"
by(rule sup_plus, rule non, rule bddF, rule bddG)
moreover have "... ≤ (SUP xa∈ R. f x xa) + (∑i∈F. SUP a∈R. f i a)"
using add_le_cancel_left conts insert.hyps(3) by blast
moreover have "... ≤ (∑i∈(insert x F). SUP a∈R. f i a)"
by (simp add: insert.hyps(2))
ultimately have "((SUP xa∈R. ∑i∈insert x F. f i xa)::real) ≤ (∑i∈(insert x F). SUP a∈R. f i a)"
by linarith
then show ?case by auto
qed
qed
have SUP_sum_comm:"⋀R S y1 y2 . finite (S::'a set) ⟹ (R::'b set) ≠ {} ⟹ (SUP x∈R . (∑i ∈ S. norm(f i y1 x - f i y2 x)/norm(x))) ≤ (∑i ∈ S. (SUP x∈R. norm(f i y1 x - f i y2 x)/norm(x)))"
apply(rule SUP_sum_comm')
apply(auto)[3]
proof (unfold bdd_above_def)
fix R S y1 y2 i
{ fix rr :: "real ⇒ real"
obtain bb :: "real ⇒ ('b ⇒ real) ⇒ 'b set ⇒ 'b" where
ff1: "⋀r f B. r ∉ f ` B ∨ f (bb r f B) = r"
unfolding image_iff by moura
{ assume "∃r. ¬ rr r ≤ norm (f i y1 - f i y2)"
then have "∃r. norm (blinfun_apply (f i y1) (bb (rr r) (λb. norm (blinfun_apply (f i y1) b - blinfun_apply (f i y2) b) / norm b) R) - blinfun_apply (f i y2) (bb (rr r) (λb. norm (blinfun_apply (f i y1) b - blinfun_apply (f i y2) b) / norm b) R)) / norm (bb (rr r) (λb. norm (blinfun_apply (f i y1) b - blinfun_apply (f i y2) b) / norm b) R) ≠ rr r"
by (metis (no_types) le_norm_blinfun minus_blinfun.rep_eq)
then have "∃r. rr r ≤ r ∨ rr r ∉ (λb. norm (blinfun_apply (f i y1) b - blinfun_apply (f i y2) b) / norm b) ` R"
using ff1 by meson }
then have "∃r. rr r ≤ r ∨ rr r ∉ (λb. norm (blinfun_apply (f i y1) b - blinfun_apply (f i y2) b) / norm b) ` R"
by blast }
then show "∃r. ∀ra∈(λb. norm (blinfun_apply (f i y1) b - blinfun_apply (f i y2) b) / norm b) ` R. ra ≤ r"
by meson
qed
have SUM_leq:"⋀S::('a) set. ⋀ f g ::('a ⇒ real). S ≠ {} ⟹ finite S ⟹ (⋀x. x ∈ S ⟹ f x < g x) ⟹ (∑x∈S. f x) < (∑x∈S. g x)"
by(rule sum_strict_mono, auto)
have L2:"⋀f S. L2_set (λx. norm(f x)) S ≤ (∑x ∈ S. norm(f x))"
using L2_set_le_sum norm_ge_zero by metis
have L2':"⋀y. (L2_set (λi. norm(f i x1 y - f i x2 y)) UNIV)/norm(y) ≤ (∑i∈UNIV. norm(f i x1 y - f i x2 y))/norm(y)"
subgoal for y
using L2[of "(λ x. f x x1 y - f x x2 y)" UNIV]
by (auto simp add: divide_right_mono)
done
have "⋀i. (SUP y∈UNIV. norm((f i x1 - f i x2) y)/norm(y)) = norm(f i x1 - f i x2)"
by (simp add: onorm_def norm_blinfun.rep_eq)
then have each_norm:"⋀i. (SUP y∈UNIV. norm(f i x1 y - f i x2 y)/norm(y)) = norm(f i x1 - f i x2)"
by (metis (no_types, lifting) SUP_cong blinfun.diff_left)
have bounded_linear:"⋀i. bounded_linear (λy. f i x1 y - f i x2 y)"
by (simp add: blinfun.bounded_linear_right bounded_linear_sub)
have each_bound:"⋀i. bdd_above ((λy. norm(f i x1 y - f i x2 y)/norm(y)) ` UNIV)"
using bounded_linear unfolding bdd_above_def
proof -
fix i :: 'a
{ fix rr :: "real ⇒ real"
have "⋀a r. norm (blinfun_apply (f a x1) r - blinfun_apply (f a x2) r) / norm r ≤ norm (f a x1 - f a x2)"
by (metis le_norm_blinfun minus_blinfun.rep_eq)
then have "⋀r R. r ∉ (λr. norm (blinfun_apply (f i x1) r - blinfun_apply (f i x2) r) / norm r) ` R ∨ r ≤ norm (f i x1 - f i x2)"
by blast
then have "∃r. rr r ≤ r ∨ rr r ∉ range (λr. norm (blinfun_apply (f i x1) r - blinfun_apply (f i x2) r) / norm r)"
by blast }
then show "∃r. ∀ra∈range (λr. norm (blinfun_apply (f i x1) r - blinfun_apply (f i x2) r) / norm r). ra ≤ r"
by meson
qed
have bdd_above:"(bdd_above ((λy. (∑i∈UNIV. norm(f i x1 y - f i x2 y)/norm(y))) ` UNIV))"
using each_bound unfolding bdd_above_def apply auto
proof -
assume each:"(⋀i. ∃M. ∀x. ¦blinfun_apply (f i x1) x - blinfun_apply (f i x2) x¦ / norm x ≤ M)"
let ?boundP = "(λi M. ∀x. ¦blinfun_apply (f i x1) x - blinfun_apply (f i x2) x¦ / norm x ≤ M)"
let ?bound = "(λi. SOME x. ?boundP i x)"
have bounds:"⋀i. ?boundP i (?bound i)"
subgoal for i using each someI[of "?boundP i"] by blast done
let ?bigBound = "∑i∈(UNIV::'a set). ?bound i"
show "∃M. ∀x. (∑i∈UNIV. ¦blinfun_apply (f i x1) x - blinfun_apply (f i x2) x¦ / norm x) ≤ M"
apply(rule exI[where x= ?bigBound])
by(auto simp add: bounds sum_mono)
qed
have bdd_above:"(bdd_above ((λy. (∑i∈UNIV. norm(f i x1 y - f i x2 y))/norm(y)) ` UNIV))"
using bdd_above unfolding bdd_above_def apply auto
proof -
fix M :: real
assume a1: "∀x. (∑i∈UNIV. ¦blinfun_apply (f i x1) x - blinfun_apply (f i x2) x¦ / norm x) ≤ M"
{ fix bb :: "real ⇒ 'b"
have "⋀b. (∑a∈UNIV. ¦blinfun_apply (f a x1) b - blinfun_apply (f a x2) b¦) / norm b ≤ M"
using a1 by (simp add: sum_divide_distrib)
then have "∃r. (∑a∈UNIV. ¦blinfun_apply (f a x1) (bb r) - blinfun_apply (f a x2) (bb r)¦) / norm (bb r) ≤ r"
by blast }
then show "∃r. ∀b. (∑a∈UNIV. ¦blinfun_apply (f a x1) b - blinfun_apply (f a x2) b¦) / norm b ≤ r"
by meson
qed
have "dist (?f x2) (?f x1) = norm((?f x2) - (?f x1))"
by (simp add: dist_blinfun_def)
moreover have "... = (SUP y∈UNIV. norm(?f x1 y - ?f x2 y)/norm(y))"
by (metis (no_types, lifting) SUP_cong blinfun.diff_left norm_blinfun.rep_eq norm_minus_commute onorm_def)
moreover have "... = (SUP y∈UNIV. (L2_set (λi. norm(f i x1 y - f i x2 y)) UNIV)/norm(y))"
using euclid by auto
moreover have "... ≤ (SUP y∈UNIV. (∑i∈UNIV. norm(f i x1 y - f i x2 y))/norm(y))"
using L2' SUP_cong SUP_leq bdd_above by auto
moreover have "... = (SUP y∈UNIV. (∑i∈UNIV. norm(f i x1 y - f i x2 y)/norm(y)))"
by (simp add: sum_divide_distrib)
moreover have "... ≤ (∑i∈UNIV. (SUP y∈UNIV. norm(f i x1 y - f i x2 y)/norm(y)))"
by(rule SUP_sum_comm[OF finite nonemptyB, of x1 x2])
moreover have "... = (∑i∈UNIV. norm(f i x1 - f i x2))"
using each_norm by simp
moreover have "... = (∑i∈UNIV. dist(f i x1) (f i x2))"
by (simp add: dist_blinfun_def)
moreover have "... < (∑i∈(UNIV::'a set). ε / ?n)"
using conts'''[OF ne dists] using SUM_leq[OF nonempty, of "(λi. dist (f i x1) (f i x2))" "(λi. ε / ?n)"]
by (simp add: dist_commute)
moreover have "... = ε"
by(auto)
ultimately show "dist (?f x2) (?f x1) < ε"
by linarith
qed
then show "∃s>0. ∀x2. x2 ≠ x1 ∧ dist x2 x1 < s ⟶ dist (blinfun_vec (λi. f i x2)) (blinfun_vec (λi. f i x1)) < ε"
using δ by blast
qed
lemma has_derivative_vec[derivative_intros]:
assumes "⋀i. ((λx. f i x) has_derivative (λh. f' i h)) F"
shows "((λx. χ i. f i x) has_derivative (λh. χ i. f' i h)) F"
proof -
have *: "(χ i. f i x) = (∑i∈UNIV. axis i (f i x))" "(χ i. f' i x) = (∑i∈UNIV. axis i (f' i x))" for x
by (simp_all add: axis_def sum.If_cases vec_eq_iff)
show ?thesis
unfolding *
by (intro has_derivative_sum bounded_linear.has_derivative[OF bounded_linear_axis] assms)
qed
lemma has_derivative_proj:
fixes j::"('a::finite)"
fixes f::"'a ⇒ real ⇒ real"
assumes assm:"((λx. χ i. f i x) has_derivative (λh. χ i. f' i h)) F"
shows "((λx. f j x) has_derivative (λh. f' j h)) F"
proof -
have bounded_proj:"bounded_linear (λ x::(real^'a). x $ j)"
by (simp add: bounded_linear_vec_nth)
show "?thesis"
using bounded_linear.has_derivative[OF bounded_proj, of "(λx. χ i. f i x)" "(λh. χ i. f' i h)", OF assm]
by auto
qed
lemma has_derivative_proj':
fixes i::"'a::finite"
shows "∀x. ((λ x. x $ i) has_derivative (λx::(real^'a). x $ i)) (at x)"
proof -
have bounded_proj:"bounded_linear (λ x::(real^'a). x $ i)"
by (simp add: bounded_linear_vec_nth)
show "?thesis"
using bounded_proj unfolding has_derivative_def by auto
qed
lemma constant_when_zero:
fixes v::"real ⇒ (real, 'i::finite) vec"
assumes x0: "(v t0) $ i = x0"
assumes sol: "(v solves_ode f) T S"
assumes f0: "⋀s x. s ∈ T ⟹ f s x $ i = 0"
assumes t0:"t0 ∈ T"
assumes t:"t ∈ T"
assumes convex:"convex T"
shows "v t $ i = x0"
proof -
from solves_odeD[OF sol]
have deriv: "(v has_vderiv_on (λt. f t (v t))) T" by simp
then have "((λt. v t $ i) has_vderiv_on (λt. 0)) T"
using f0
by (auto simp: has_vderiv_on_def has_vector_derivative_def cart_eq_inner_axis
intro!: derivative_eq_intros)
from has_vderiv_on_zero_constant[OF convex this]
obtain c where c:"⋀x. x ∈ T ⟹ v x $ i = c" by blast
with x0 have "c = x0" "v t $ i = c"
using t t0 c x0 by blast+
then show ?thesis by simp
qed
lemma
solves_ode_subset:
assumes x: "(x solves_ode f) T X"
assumes s: "S ⊆ T"
shows "(x solves_ode f) S X"
apply(rule solves_odeI)
using has_vderiv_on_subset s solves_ode_vderivD x apply force
using assms by (auto intro!: solves_odeI dest!: solves_ode_domainD)
lemma
solves_ode_supset_range:
assumes x: "(x solves_ode f) T X"
assumes y: "X ⊆ Y"
shows "(x solves_ode f) T Y"
apply(rule solves_odeI)
using has_vderiv_on_subset y solves_ode_vderivD x apply force
using assms by (auto intro!: solves_odeI dest!: solves_ode_domainD)
lemma
usolves_ode_subset:
assumes x: "(x usolves_ode f from t0) T X"
assumes s: "S ⊆ T"
assumes t0: "t0 ∈ S"
assumes S: "is_interval S"
shows "(x usolves_ode f from t0) S X"
proof (rule usolves_odeI)
note usolves_odeD[OF x]
show "(x solves_ode f) S X" by (rule solves_ode_subset; fact)
show "t0 ∈ S" "is_interval S" by(fact+)
fix z t
assume s: "{t0 -- t} ⊆ S" and z: "(z solves_ode f) {t0 -- t} X" and z0: "z t0 = x t0"
then have "t0 ∈ {t0 -- t}" "is_interval {t0 -- t}"
by auto
moreover note s
moreover have "(z solves_ode f) {t0--t} X"
using solves_odeD[OF z] ‹S ⊆ T›
by (intro solves_ode_subset_range[OF z]) force
moreover note z0
moreover have "t ∈ {t0 -- t}" by simp
ultimately show "z t = x t"
by (meson ‹⋀z ta T'. ⟦t0 ∈ T'; is_interval T'; T' ⊆ T; (z solves_ode f) T' X; z t0 = x t0; ta ∈ T'⟧ ⟹ z ta = x ta› assms(2) dual_order.trans)
qed
lemma example:
fixes x t::real and i::"('sz::finite)"
assumes "t > 0"
shows "x = (ll_on_open.flow UNIV (λt. λx. χ (i::('sz::finite)). 0) UNIV 0 (χ i. x) t) $ i"
proof -
let ?T = UNIV
let ?f = "(λt. λx. χ i::('sz::finite). 0)"
let ?X = UNIV
let ?t0.0 = 0
let ?x0.0 = "χ i::('sz::finite). x"
interpret ll: ll_on_open "UNIV" "(λt x. χ i::('sz::finite). 0)" UNIV
using gt_ex
by unfold_locales
(auto simp: interval_def continuous_on_def local_lipschitz_def intro!: lipschitz_intros)
have foo1:"?t0.0 ∈ ?T" by auto
have foo2:"?x0.0 ∈ ?X" by auto
let ?v = "ll.flow ?t0.0 ?x0.0"
from ll.flow_solves_ode[OF foo1 foo2]
have solves:"(ll.flow ?t0.0 ?x0.0 solves_ode ?f) (ll.existence_ivl ?t0.0 ?x0.0) ?X" by (auto)
then have solves:"(?v solves_ode ?f) (ll.existence_ivl ?t0.0 ?x0.0) ?X" by auto
have thex0: "(?v ?t0.0) $ (i::('sz::finite)) = x" by auto
have sol_help: "(?v solves_ode ?f) (ll.existence_ivl ?t0.0 ?x0.0) ?X" using solves by auto
have ivl:"ll.existence_ivl ?t0.0 ?x0.0 = UNIV"
by (rule ll.existence_ivl_eq_domain)
(auto intro!: exI[where x=0] simp: vec_eq_iff)
have sol: "(?v solves_ode ?f) UNIV ?X" using solves ivl by auto
have thef0: "⋀t x. ?f t x $ i = 0" by auto
from constant_when_zero [OF thex0 sol thef0]
have "?v t $ i = x"
by auto
thus ?thesis by auto
qed
lemma MVT_ivl:
fixes f::"'a::ordered_euclidean_space⇒'b::ordered_euclidean_space"
assumes fderiv: "⋀x. x ∈ D ⟹ (f has_derivative J x) (at x within D)"
assumes J_ivl: "⋀x. x ∈ D ⟹ J x u ≥ J0"
assumes line_in: "⋀x. x ∈ {0..1} ⟹ a + x *⇩R u ∈ D"
shows "f (a + u) - f a ≥ J0"
proof -
from MVT_corrected[OF fderiv line_in] obtain t where
t: "t∈Basis → {0<..<1}" and
mvt: "f (a + u) - f a = (∑i∈Basis. (J (a + t i *⇩R u) u ∙ i) *⇩R i)"
by auto
note mvt
also have "… ≥ J0"
proof -
have J: "⋀i. i ∈ Basis ⟹ J0 ≤ J (a + t i *⇩R u) u"
using J_ivl t line_in by (auto simp: Pi_iff)
show ?thesis
using J
unfolding atLeastAtMost_iff eucl_le[where 'a='b]
by auto
qed
finally show ?thesis .
qed
lemma MVT_ivl':
fixes f::"'a::ordered_euclidean_space⇒'b::ordered_euclidean_space"
assumes fderiv: "(⋀x. x ∈ D ⟹ (f has_derivative J x) (at x within D))"
assumes J_ivl: "⋀x. x ∈ D ⟹ J x (a - b) ≥ J0"
assumes line_in: "⋀x. x ∈ {0..1} ⟹ b + x *⇩R (a - b) ∈ D"
shows "f a ≥ f b + J0"
proof -
have "f (b + (a - b)) - f b ≥ J0"
apply (rule MVT_ivl[OF fderiv ])
apply assumption
apply (rule J_ivl) apply assumption
using line_in
apply (auto simp: diff_le_eq le_diff_eq ac_simps)
done
thus ?thesis
by (auto simp: diff_le_eq le_diff_eq ac_simps)
qed
end