Theory ODE_Misc
section ‹Additions to the ODE Library›
theory ODE_Misc
imports
Ordinary_Differential_Equations.ODE_Analysis
Analysis_Misc
begin
lemma local_lipschitz_compact_bicomposeE:
assumes ll: "local_lipschitz T X f"
assumes cf: "⋀x. x ∈ X ⟹ continuous_on I (λt. f t x)"
assumes cI: "compact I"
assumes "I ⊆ T"
assumes cv: "continuous_on I v"
assumes cw: "continuous_on I w"
assumes v: "v ` I ⊆ X"
assumes w: "w ` I ⊆ X"
obtains L where "L > 0" "⋀x. x ∈ I ⟹ dist (f x (v x)) (f x (w x)) ≤ L * dist (v x) (w x)"
proof -
from v w have "v ` I ∪ w ` I ⊆ X" by auto
with ll ‹I ⊆ T› have llI:"local_lipschitz I (v ` I ∪ w ` I) f"
by (rule local_lipschitz_subset)
have cvwI: "compact (v ` I ∪ w ` I)"
by (auto intro!: compact_continuous_image cv cw cI)
from local_lipschitz_compact_implies_lipschitz[OF llI cvwI ‹compact I› cf]
obtain L where L: "⋀t. t ∈ I ⟹ L-lipschitz_on (v ` I ∪ w ` I) (f t)"
using v w
by blast
define L' where "L' = max L 1"
with L have "L' > 0" "⋀x. x ∈ I ⟹ dist (f x (v x)) (f x (w x)) ≤ L' * dist (v x) (w x)"
apply (auto simp: lipschitz_on_def L'_def)
by (smt Un_iff image_eqI mult_right_mono zero_le_dist)
then show ?thesis ..
qed
subsection ‹Comparison Principle›
lemma comparison_principle_le:
fixes f::"real ⇒ real ⇒ real"
and φ ψ::"real ⇒ real"
assumes ll: "local_lipschitz X Y f"
assumes cf: "⋀x. x ∈ Y ⟹ continuous_on {a..b} (λt. f t x)"
assumes abX: "{a .. b} ⊆ X"
assumes φ': "⋀x. x ∈ {a .. b} ⟹ (φ has_real_derivative φ' x) (at x)"
assumes ψ': "⋀x. x ∈ {a .. b} ⟹ (ψ has_real_derivative ψ' x) (at x)"
assumes φ_in: "φ ` {a..b} ⊆ Y"
assumes ψ_in: "ψ ` {a..b} ⊆ Y"
assumes init: "φ a ≤ ψ a"
assumes defect: "⋀x. x ∈ {a .. b} ⟹ φ' x - f x (φ x) ≤ ψ' x - f x (ψ x)"
shows "∀x ∈ {a .. b}. φ x ≤ ψ x" (is "?th1")
unfolding atomize_conj
apply (cases "a ≤ b")
defer subgoal by simp
proof -
assume "a ≤ b"
note φ_cont = has_real_derivative_imp_continuous_on[OF φ']
note ψ_cont = has_real_derivative_imp_continuous_on[OF ψ']
from local_lipschitz_compact_bicomposeE[OF ll cf compact_Icc abX φ_cont ψ_cont φ_in ψ_in]
obtain L where L: "L > 0" "⋀x. x ∈ {a..b} ⟹ dist (f x (φ x)) (f x (ψ x)) ≤ L * dist (φ x) (ψ x)" by blast
define w where "w x = ψ x - φ x" for x
have w'[derivative_intros]: "⋀x. x ∈ {a .. b} ⟹ (w has_real_derivative ψ' x - φ' x) (at x)"
using φ' ψ'
by (auto simp: has_vderiv_on_def w_def[abs_def] intro!: derivative_eq_intros)
note w_cont[continuous_intros] = has_real_derivative_imp_continuous_on[OF w', THEN continuous_on_compose2]
have "w d ≥ 0" if "d ∈ {a .. b}" for d
proof (rule ccontr, unfold not_le)
assume "w d < 0"
let ?N = "(w -` {..0} ∩ {a .. d})"
from ‹w d < 0› that have "d ∈ ?N" by auto
then have "?N ≠ {}" by auto
have "closed ?N"
unfolding compact_eq_bounded_closed
using that
by (intro conjI closed_vimage_Int) (auto intro!: continuous_intros)
let ?N' = "{a0 ∈ {a .. d}. w ` {a0 .. d} ⊆ {..0}}"
from ‹w d < 0› that have "d ∈ ?N'" by simp
then have "?N' ≠ {}" by auto
have "compact ?N'"
unfolding compact_eq_bounded_closed
proof
have "?N' ⊆ {a .. d}" using that by auto
then show "bounded ?N'"
by (rule bounded_subset[rotated]) simp
have "w u ≤ 0" if "(∀n. x n ∈ ?N')" "x ⇢ l" "l ≤ u" "u ≤ d" for x l u
proof cases
assume "l = u"
have "∀n. x n ∈ ?N" using that(1) by force
from closed_sequentially[OF ‹closed ?N›] this ‹x ⇢ l›
show ?thesis
using ‹l = u› by blast
next
assume "l ≠ u" with that have "l < u" by auto
from order_tendstoD(2)[OF ‹x ⇢ l› ‹l < u›] obtain n where "x n < u"
by (auto dest: eventually_happens)
with that show ?thesis using ‹l < u›
by (auto dest!: spec[where x=n] simp: image_subset_iff)
qed
then show "closed ?N'"
unfolding closed_sequential_limits
by (auto simp: Lim_bounded Lim_bounded2)
qed
from compact_attains_inf[OF ‹compact ?N'› ‹?N' ≠ {}›]
obtain a0 where a0: "a ≤ a0" "a0 ≤ d" "w ` {a0..d} ⊆ {..0}"
and a0_least: "⋀x. a ≤ x ⟹ x ≤ d ⟹ w ` {x..d} ⊆ {..0} ⟹ a0 ≤ x"
by auto
have a0d: "{a0 .. d} ⊆ {a .. b}" using that a0
by auto
have L_w_bound: "L * w x ≤ ψ' x - φ' x" if "x ∈ {a0 .. d}" for x
proof -
from set_mp[OF a0d that] have "x ∈ {a .. b}" .
from defect[OF this]
have "φ' x - ψ' x ≤ dist (f x (φ x)) (f x (ψ x))"
by (simp add: dist_real_def)
also have "… ≤ L * dist (φ x) (ψ x)"
using ‹x ∈ {a .. b}›
by (rule L)
also have "… ≤ -L * w x"
using ‹0 < L› a0 that
by (force simp add: dist_real_def abs_real_def w_def algebra_split_simps )
finally show ?thesis
by simp
qed
have mono: "mono_on {a0..d} (λx. w x * exp(-L*x))"
apply (rule mono_onI)
apply (rule DERIV_nonneg_imp_nondecreasing, assumption)
using a0d
by (auto intro!: exI[where x="(ψ' x - φ' x) * exp (- (L * x)) - exp (- (L * x)) * L * w x" for x]
derivative_eq_intros L_w_bound simp: )
then have "w a0 * exp (-L * a0) ≤ w d * exp (-L * d)"
by (rule mono_onD) (use that a0 in auto)
also have "… < 0" using ‹w d < 0› by (simp add: algebra_split_simps)
finally have "w a0 * exp (- L * a0) < 0" .
then have "w a0 < 0" by (simp add: algebra_split_simps)
have "a0 ≤ a"
proof (rule ccontr, unfold not_le)
assume "a < a0"
have "continuous_on {a.. a0} w"
by (rule continuous_intros, assumption) (use a0 a0d in auto)
from continuous_on_Icc_at_leftD[OF this ‹a < a0›]
have "(w ⤏ w a0) (at_left a0)" .
from order_tendstoD(2)[OF this ‹w a0 < 0›] have "∀⇩F x in at_left a0. w x < 0" .
moreover have "∀⇩F x in at_left a0. a < x"
by (rule order_tendstoD) (auto intro!: ‹a < a0›)
ultimately have "∀⇩F x in at_left a0. a < x ∧ w x < 0" by eventually_elim auto
then obtain a1' where "a1'<a0" and a1_neg: "⋀y. y > a1' ⟹ y < a0 ⟹ a < y ∧ w y < 0"
unfolding eventually_at_left_field by auto
define a1 where "a1 = (a1' + a0)/2"
have "a1 < a0" using ‹a1' < a0› by (auto simp: a1_def)
have "a ≤ a1"
using ‹a < a0› a1_neg by (force simp: a1_def)
moreover have "a1 ≤ d"
using ‹a1' < a0› a0(2) by (auto simp: a1_def)
moreover have "w ` {a1..a0} ⊆ {..0}"
using ‹w a0 < 0› a1_neg a0(3)
by (auto simp: a1_def) smt
moreover have "w ` {a0..d} ⊆ {..0}" using a0 by auto
ultimately
have "a0 ≤ a1"
apply (intro a0_least) apply assumption apply assumption
by (smt atLeastAtMost_iff image_subset_iff)
with ‹a1<a0› show False by simp
qed
then have "a0 = a" using ‹a ≤ a0› by simp
with ‹w a0 < 0› have "w a < 0" by simp
with init show False
by (auto simp: w_def)
qed
then show ?thesis
by (auto simp: w_def)
qed
lemma local_lipschitz_mult:
shows "local_lipschitz (UNIV::real set) (UNIV::real set) (*)"
apply (auto intro!: c1_implies_local_lipschitz[where f'="λp. blinfun_mult_left (fst p)"])
apply (simp add: has_derivative_mult_right mult_commute_abs)
by (auto intro!: continuous_intros)
lemma comparison_principle_le_linear:
fixes φ :: "real ⇒ real"
assumes "continuous_on {a..b} g"
assumes "(⋀t. t ∈ {a..b} ⟹ (φ has_real_derivative φ' t) (at t))"
assumes "φ a ≤ 0"
assumes "(⋀t. t ∈ {a..b} ⟹ φ' t ≤ g t *⇩R φ t)"
shows "∀t∈{a..b}. φ t ≤ 0"
proof -
have *: "⋀x. continuous_on {a..b} (λt. g t * x)"
using assms(1) continuous_on_mult_right by blast
then have "local_lipschitz (g`{a..b}) UNIV (*)"
using local_lipschitz_subset[OF local_lipschitz_mult] by blast
from local_lipschitz_compose1[OF this assms(1)]
have "local_lipschitz {a..b} UNIV (λt. (*) (g t))" .
from comparison_principle_le[OF this _ _ assms(2) _ _ _ assms(3), of b "λt.0"] * assms(4)
show ?thesis by auto
qed
subsection ‹Locally Lipschitz ODEs›
context ll_on_open_it begin
lemma flow_lipschitzE:
assumes "{a .. b} ⊆ existence_ivl t0 x"
obtains L where "L-lipschitz_on {a .. b} (flow t0 x)"
proof -
have f': "(flow t0 x has_derivative (λi. i *⇩R f t (flow t0 x t))) (at t within {a .. b})" if "t ∈ {a .. b}" for t
using flow_has_derivative[of t x] assms that
by (auto simp: has_derivative_at_withinI)
have "compact ((λt. f t (flow t0 x t)) ` {a .. b})"
using assms
apply (auto intro!: compact_continuous_image continuous_intros)
using local.existence_ivl_empty2 apply fastforce
apply (meson atLeastAtMost_iff general.existence_ivl_subset in_mono)
by (simp add: general.flow_in_domain subset_iff)
then obtain C where "t ∈ {a .. b} ⟹ norm (f t (flow t0 x t)) ≤ C" for t
by (fastforce dest!: compact_imp_bounded simp: bounded_iff intro: that)
then have "t ∈ {a..b} ⟹ onorm (λi. i *⇩R f t (flow t0 x t)) ≤ max 0 C" for t
apply (subst onorm_scaleR_left)
apply (auto simp: onorm_id max_def)
by (metis diff_0_right diff_mono diff_self norm_ge_zero)
from bounded_derivative_imp_lipschitz[OF f' _ this]
have "(max 0 C)-lipschitz_on {a..b} (flow t0 x)"
by auto
then show ?thesis ..
qed
lemma flow_undefined0: "t ∉ existence_ivl t0 x ⟹ flow t0 x t = 0"
unfolding flow_def by auto
lemma csols_undefined: "x ∉ X ⟹ csols t0 x = {}"
apply (auto simp: csols_def)
using general.existence_ivl_empty2 general.existence_ivl_maximal_segment
apply blast
done
lemmas existence_ivl_undefined = existence_ivl_empty2
end
subsection ‹Reverse flow as Sublocale›
lemma range_preflect_0[simp]: "range (preflect 0) = UNIV"
by (auto simp: preflect_def)
lemma range_uminus[simp]: "range uminus = (UNIV::'a::ab_group_add set)"
by auto
context auto_ll_on_open begin
sublocale rev: auto_ll_on_open "-f" rewrites "-(-f) = f"
apply unfold_locales
using auto_local_lipschitz auto_open_domain
unfolding fun_Compl_def local_lipschitz_minus
by auto
lemma existence_ivl_eq_rev0: "existence_ivl0 y = uminus ` rev.existence_ivl0 y" for y
by (auto simp: existence_ivl_eq_rev rev.existence_ivl0_def preflect_def)
lemma rev_existence_ivl_eq0: "rev.existence_ivl0 y = uminus ` existence_ivl0 y" for y
using uminus_uminus_image[of "rev.existence_ivl0 y"]
by (simp add: existence_ivl_eq_rev0)
lemma flow_eq_rev0: "flow0 y t = rev.flow0 y (-t)" for y t
apply (cases "t ∈ existence_ivl0 y")
subgoal
apply (subst flow_eq_rev(2), assumption)
apply (subst rev.flow0_def)
by (simp add: preflect_def)
subgoal
apply (frule flow_undefined0)
by (auto simp: existence_ivl_eq_rev0 rev.flow_undefined0)
done
lemma rev_eq_flow: "rev.flow0 y t = flow0 y (-t)" for y t
apply (subst flow_eq_rev0)
using uminus_uminus_image[of "rev.existence_ivl0 y"]
apply -
apply (subst (asm) existence_ivl_eq_rev0[symmetric])
by auto
lemma rev_flow_image_eq: "rev.flow0 x ` S = flow0 x ` (uminus ` S)"
unfolding rev_eq_flow[abs_def]
by force
lemma flow_image_eq_rev: "flow0 x ` S = rev.flow0 x ` (uminus ` S)"
unfolding rev_eq_flow[abs_def]
by force
end
context c1_on_open begin
sublocale rev: c1_on_open "-f" "-f'" rewrites "-(-f) = f" and "-(-f') = f'"
by (rule c1_on_open_rev) auto
end
context c1_on_open_euclidean begin
sublocale rev: c1_on_open_euclidean "-f" "-f'" rewrites "-(-f) = f" and "-(-f') = f'"
by unfold_locales auto
end
subsection ‹Autonomous LL ODE : Existence Interval and trapping on the interval›
lemma bdd_above_is_intervalI: "bdd_above I"
if "is_interval I" "a ≤ b" "a ∈ I" "b ∉ I" for I::"real set"
by (meson bdd_above_def is_interval_1 le_cases that)
lemma bdd_below_is_intervalI: "bdd_below I"
if "is_interval I" "a ≤ b" "a ∉ I" "b ∈ I" for I::"real set"
by (meson bdd_below_def is_interval_1 le_cases that)
context auto_ll_on_open begin
lemma open_existence_ivl0:
assumes x : "x ∈ X"
shows "∃a b. a < 0 ∧ 0 < b ∧ {a..b} ⊆ existence_ivl0 x"
proof -
have a1:"0 ∈ existence_ivl0 x"
by (simp add: x)
have a2: "open (existence_ivl0 x)"
by (simp add: x)
from a1 a2 obtain d where "d > 0" "ball 0 d ⊆ existence_ivl0 x"
using openE by blast
have "{-d/2..d/2} ⊆ ball 0 d"
using ‹0 < d› dist_norm mem_ball by auto
thus ?thesis
by (smt ‹0 < d› ‹ball 0 d ⊆ existence_ivl0 x› divide_minus_left half_gt_zero order_trans)
qed
lemma open_existence_ivl':
assumes x : "x ∈ X"
obtains a where "a > 0" "{-a..a} ⊆ existence_ivl0 x"
proof -
from open_existence_ivl0[OF assms(1)]
obtain a b where ab: "a < 0" "0 < b" "{a..b} ⊆ existence_ivl0 x" by auto
then have "min (-a) b > 0" by linarith
have "{-min (-a) b .. min(-a) b} ⊆ {a..b}" by auto
thus ?thesis using ab(3) that[OF ‹min (-a) b > 0›] by blast
qed
lemma open_existence_ivl_on_compact:
assumes C: "C ⊆ X" and "compact C" "C ≠ {}"
obtains a where "a > 0" "⋀x. x ∈ C ⟹ {-a..a} ⊆ existence_ivl0 x"
proof -
from existence_ivl_cballs
have "∀x∈C. ∃e>0. ∃t>0. ∀y∈cball x e. cball 0 t⊆existence_ivl0 y"
by (metis (full_types) C Int_absorb1 Int_iff UNIV_I)
then
obtain d' t' where *:
"∀x∈C. 0 < d' x ∧ t' x > 0 ∧ (∀y∈cball x (d' x). cball 0 (t' x) ⊆ existence_ivl0 y)"
by metis
with compactE_image[OF ‹compact C›, of C "λx. ball x (d' x)"]
obtain C' where "C' ⊆ C" and [simp]: "finite C'" and C_subset: "C ⊆ (⋃c∈C'. ball c (d' c))"
by force
from C_subset ‹C ≠ {}› have [simp]: "C' ≠ {}" by auto
define d where "d = Min (d' ` C')"
define t where "t = Min (t' ` C')"
have "t > 0" using * ‹C' ⊆ C›
by (auto simp: t_def)
moreover have "{-t .. t} ⊆ existence_ivl0 x" if "x ∈ C" for x
proof -
from C_subset that ‹C' ⊆ C›
obtain c where c: "c ∈ C'" "x ∈ ball c (d' c)" "c ∈ C" by force
then have "{-t .. t} ⊆ cball 0 (t' c)"
by (auto simp: abs_real_def t_def minus_le_iff)
also
from c have "cball 0 (t' c) ⊆ existence_ivl0 x"
using *[rule_format, OF ‹c ∈ C›] by auto
finally show ?thesis .
qed
ultimately show ?thesis ..
qed
definition "trapped_forward x K ⟷ (flow0 x ` (existence_ivl0 x ∩ {0..}) ⊆ K)"
definition "trapped_backward x K ⟷ (flow0 x ` (existence_ivl0 x ∩ {..0}) ⊆ K)"
definition "trapped x K ⟷ trapped_forward x K ∧ trapped_backward x K"
lemma trapped_iff_on_existence_ivl0:
"trapped x K ⟷ (flow0 x ` (existence_ivl0 x) ⊆ K)"
unfolding trapped_def trapped_forward_def trapped_backward_def
apply (auto)
by (metis IntI atLeast_iff atMost_iff image_subset_iff less_eq_real_def linorder_not_less)
end
context auto_ll_on_open begin
lemma infinite_rev_existence_ivl0_rewrites:
"{0..} ⊆ rev.existence_ivl0 x ⟷ {..0} ⊆ existence_ivl0 x"
"{..0} ⊆ rev.existence_ivl0 x ⟷ {0..} ⊆ existence_ivl0 x"
apply (auto simp add: rev.rev_existence_ivl_eq0 subset_iff)
using neg_le_0_iff_le apply fastforce
using neg_0_le_iff_le by fastforce
lemma trapped_backward_iff_rev_trapped_forward:
"trapped_backward x K ⟷ rev.trapped_forward x K"
unfolding trapped_backward_def rev.trapped_forward_def
by (auto simp add: rev_flow_image_eq existence_ivl_eq_rev0 image_subset_iff)
text ‹If solution is trapped in a compact set at some time
on its existence interval then it is trapped forever›
lemma trapped_sol_right:
assumes "compact K" "K ⊆ X"
assumes "x ∈ X" "trapped_forward x K"
shows "{0..} ⊆ existence_ivl0 x"
proof (rule ccontr)
assume "¬ {0..} ⊆ existence_ivl0 x"
from this obtain t where "0 ≤ t" "t ∉ existence_ivl0 x" by blast
then have bdd: "bdd_above (existence_ivl0 x)"
by (auto intro!: bdd_above_is_intervalI ‹x ∈ X›)
from flow_leaves_compact_ivl_right [OF UNIV_I ‹x ∈ X› bdd UNIV_I assms(1-2)]
show False by (metis assms(4) trapped_forward_def IntI atLeast_iff image_subset_iff)
qed
lemma trapped_sol_right_gen:
assumes "compact K" "K ⊆ X"
assumes "t ∈ existence_ivl0 x" "trapped_forward (flow0 x t) K"
shows "{t..} ⊆ existence_ivl0 x"
proof -
have "x ∈ X"
using assms(3) local.existence_ivl_empty_iff by fastforce
have xtk: "flow0 x t ∈ X"
by (simp add: assms(3) local.flow_in_domain)
from trapped_sol_right[OF assms(1-2) xtk assms(4)] have "{0..} ⊆ existence_ivl0 (flow0 x t)" .
thus "{t..} ⊆ existence_ivl0 x"
using existence_ivl_trans[OF assms(3)]
by (metis add.commute atLeast_iff diff_add_cancel le_add_same_cancel1 subset_iff)
qed
lemma trapped_sol_left:
assumes "compact K" "K ⊆ X"
assumes "x ∈ X" "trapped_backward x K"
shows "{..0} ⊆ existence_ivl0 x"
proof (rule ccontr)
assume "¬ {..0} ⊆ existence_ivl0 x"
from this obtain t where "t ≤ 0" "t ∉ existence_ivl0 x" by blast
then have bdd: "bdd_below (existence_ivl0 x)"
by (auto intro!: bdd_below_is_intervalI ‹x ∈ X›)
from flow_leaves_compact_ivl_left [OF UNIV_I ‹x ∈ X› bdd UNIV_I assms(1-2)]
show False
by (metis IntI assms(4) atMost_iff auto_ll_on_open.trapped_backward_def auto_ll_on_open_axioms image_subset_iff)
qed
lemma trapped_sol_left_gen:
assumes "compact K" "K ⊆ X"
assumes "t ∈ existence_ivl0 x" "trapped_backward (flow0 x t) K"
shows "{..t} ⊆ existence_ivl0 x"
proof -
have "x ∈ X"
using assms(3) local.existence_ivl_empty_iff by fastforce
have xtk: "flow0 x t ∈ X"
by (simp add: assms(3) local.flow_in_domain)
from trapped_sol_left[OF assms(1-2) xtk assms(4)] have "{..0} ⊆ existence_ivl0 (flow0 x t)" .
thus "{..t} ⊆ existence_ivl0 x"
using existence_ivl_trans[OF assms(3)]
by (metis add.commute add_le_same_cancel1 atMost_iff diff_add_cancel subset_eq)
qed
lemma trapped_sol:
assumes "compact K" "K ⊆ X"
assumes "x ∈ X" "trapped x K"
shows "existence_ivl0 x = UNIV"
by (metis (mono_tags, lifting) assms existence_ivl_zero image_subset_iff interval local.existence_ivl_initial_time_iff local.existence_ivl_subset local.subset_mem_compact_implies_subset_existence_interval order_refl subset_antisym trapped_iff_on_existence_ivl0)
lemma regular_locally_noteq:
assumes "x ∈ X" "f x ≠ 0"
shows "eventually (λt. flow0 x t ≠ x) (at 0)"
proof -
have nf:"norm (f x) > 0" by (simp add: assms(2))
obtain a where
a: "a>0"
"{-a--a} ⊆ existence_ivl0 x"
"0 ∈ {-a--a}"
"⋀t. t ∈ {-a--a} ⟹ norm(f (flow0 x t) - f (flow0 x 0)) ≤ norm(f x)/2"
proof -
from open_existence_ivl'[OF assms(1)]
obtain a1 where a1: "a1 > 0" "{-a1..a1} ⊆ existence_ivl0 x" .
have "continuous (at 0) (λt. norm(f (flow0 x t) - f (flow0 x 0) ))"
apply (auto intro!: continuous_intros)
by (simp add: assms(1) local.f_flow_continuous)
then obtain a2 where "a2>0"
"∀t. norm t < a2 ⟶
norm (f (flow0 x t) - f (flow0 x 0)) < norm(f x)/2"
unfolding continuous_at_real_range
by (metis abs_norm_cancel cancel_comm_monoid_add_class.diff_cancel diff_zero half_gt_zero nf norm_zero)
then have
t: "⋀t. t ∈ {-a2<--<a2} ⟹ norm(f (flow0 x t) - f (flow0 x 0)) ≤ norm(f x)/2"
by (smt open_segment_bound(2) open_segment_bound1 real_norm_def)
define a where "a = min a1 (a2/2)"
have t1:"a > 0" unfolding a_def using ‹a1 > 0› ‹a2 > 0› by auto
then have t3:"0 ∈{-a--a}"
using closed_segment_eq_real_ivl by auto
have "{-a--a} ⊆ {-a1..a1}" unfolding a_def using ‹a1 > 0› ‹a2 > 0›
using ODE_Auxiliarities.closed_segment_eq_real_ivl by auto
then have t2:"{-a--a} ⊆ existence_ivl0 x" using a1 by auto
have "{-a--a} ⊆ {-a2<--<a2}" unfolding a_def using ‹a1 > 0› ‹a2 > 0›
by (smt Diff_iff closed_segment_eq_real_ivl atLeastAtMost_iff empty_iff half_gt_zero insert_iff pos_half_less segment(1) subset_eq)
then have t4:"⋀t. t ∈ {-a--a} ⟹ norm(f (flow0 x t) - f (flow0 x 0)) ≤ norm(f x)/2" using t by auto
show ?thesis using t1 t2 t3 t4 that by auto
qed
have "⋀t. t ∈ {-a--a} ⟹ (flow0 x has_vector_derivative f (flow0 x t)) (at t within {-a--a})"
apply (rule has_vector_derivative_at_within)
using a(2) by (auto intro!:flow_has_vector_derivative)
from vector_differentiable_bound_linearization[OF this _ a(4)]
have nb:"⋀c d. {c--d} ⊆ {-a--a} ⟹
norm (flow0 x d - flow0 x c - (d - c) *⇩R f (flow0 x 0)) ≤ norm (d - c) * (norm (f x) / 2)"
using a(3) by blast
have "⋀t. dist t 0 < a ⟹ t ≠ 0 ⟹ flow0 x t ≠ x"
proof (rule ccontr)
fix t
assume "dist t 0 < a" "t ≠ 0" "¬ flow0 x t ≠ x"
then have tx:"flow0 x t = x" by auto
have "t ∈ {-a--a}"
using closed_segment_eq_real_ivl ‹dist t 0 < a› by auto
have "t > 0 ∨ t < 0" using ‹t ≠ 0› by linarith
moreover {
assume "t > 0"
then have "{0--t} ⊆ {-a--a}"
by (simp add: ‹t ∈ {-a--a}› a(3) subset_closed_segment)
from nb[OF this] have
"norm (flow0 x t - x - t *⇩R f x) ≤ norm t * (norm (f x) / 2)"
by (simp add: assms(1))
then have "norm (t *⇩R f x) ≤ norm t * (norm (f x) / 2)" using tx by auto
then have False using nf
using ‹0 < t› by auto
}
moreover {
assume "t < 0"
then have "{t--0} ⊆ {-a--a}"
by (simp add: ‹t ∈ {-a--a}› a(3) subset_closed_segment)
from nb[OF this] have
"norm (x - flow0 x t + t *⇩R f x) ≤ norm t * (norm (f x) / 2)"
by (simp add: assms(1))
then have "norm (t *⇩R f x) ≤ norm t * (norm (f x) / 2)" using tx by auto
then have False using nf
using ‹t < 0› by auto
}
ultimately show False by blast
qed
thus ?thesis unfolding eventually_at
using a(1) by blast
qed
lemma compact_max_time_flow_in_closed:
assumes "closed M" and t_ex: "t ∈ existence_ivl0 x"
shows "compact {s ∈ {0..t}. flow0 x ` {0..s} ⊆ M}" (is "compact ?C")
unfolding compact_eq_bounded_closed
proof
have "bounded {0 .. t}" by auto
then show "bounded ?C"
by (rule bounded_subset) auto
show "closed ?C"
unfolding closed_def
proof (rule topological_space_class.openI, clarsimp)
fix s
assume notM: "s ≤ t ⟶ 0 ≤ s ⟶ ¬ flow0 x ` {0..s} ⊆ M"
consider "0 ≤ s" "s ≤ t" "flow0 x s ∉ M" | "0 ≤ s" "s ≤ t" "flow0 x s ∈ M" | "s < 0" | "s > t"
by arith
then show "∃T. open T ∧ s ∈ T ∧ T ⊆ - {s. 0 ≤ s ∧ s ≤ t ∧ flow0 x ` {0..s} ⊆ M}"
proof cases
assume s: "0 ≤ s" "s ≤ t" and sM: "flow0 x s ∉ M"
have "isCont (flow0 x) s"
using s ivl_subset_existence_ivl[OF t_ex]
by (auto intro!: flow_continuous)
from this[unfolded continuous_at_open, rule_format, of "-M"] sM ‹closed M›
obtain S where "open S" "s ∈ S" "(∀x'∈S. flow0 x x' ∈ - M)"
by auto
then show ?thesis
by (force intro!: exI[where x=S])
next
assume s: "0 ≤ s" "s ≤ t" and sM: "flow0 x s ∈ M"
from this notM obtain s0 where s0: "0 ≤ s0" "s0 < s" "flow0 x s0 ∉ M"
by force
from order_tendstoD(1)[OF tendsto_ident_at ‹s0 < s›, of UNIV, unfolded eventually_at_topological]
obtain S where "open S" "s ∈ S" "⋀x. x ∈ S ⟹ x ≠ s ⟹ s0 < x"
by auto
then show ?thesis using s0
by (auto simp: intro!: exI[where x=S]) (smt atLeastAtMost_iff image_subset_iff)
qed (force intro: exI[where x="{t<..}"] exI[where x="{..<0}"])+
qed
qed
lemma flow_in_closed_max_timeE:
assumes "closed M" "t ∈ existence_ivl0 x" "0 ≤ t" "x ∈ M"
obtains T where "0 ≤ T" "T ≤ t" "flow0 x ` {0..T} ⊆ M"
"⋀s'. 0 ≤ s' ⟹ s' ≤ t ⟹ flow0 x ` {0..s'} ⊆ M ⟹ s' ≤ T"
proof -
let ?C = "{s ∈ {0..t}. flow0 x ` {0..s} ⊆ M}"
have "?C ≠ {}"
using assms
using local.mem_existence_ivl_iv_defined
by (auto intro!: exI[where x=0])
from compact_max_time_flow_in_closed[OF assms(1,2)]
have "compact ?C" .
from compact_attains_sup[OF this ‹?C ≠ {}›]
obtain s where s: "0 ≤ s" "s ≤ t" "flow0 x ` {0..s} ⊆ M"
and s_max: "⋀s'. 0 ≤ s' ⟹ s' ≤ t ⟹ flow0 x ` {0..s'} ⊆ M ⟹ s' ≤ s"
by auto
then show ?thesis ..
qed
lemma flow_leaves_closed_at_frontierE:
assumes "closed M" and t_ex: "t ∈ existence_ivl0 x" and "0 ≤ t" "x ∈ M" "flow0 x t ∉ M"
obtains s where "0 ≤ s" "s < t" "flow0 x ` {0..s} ⊆ M"
"flow0 x s ∈ frontier M"
"∃⇩F s' in at_right s. flow0 x s' ∉ M"
proof -
from flow_in_closed_max_timeE[OF assms(1-4)] assms(5)
obtain s where s: "0 ≤ s" "s < t" "flow0 x ` {0..s} ⊆ M"
and s_max: "⋀s'. 0 ≤ s' ⟹ s' ≤ t ⟹ flow0 x ` {0..s'} ⊆ M ⟹ s' ≤ s"
by (smt atLeastAtMost_iff image_subset_iff)
note s
moreover
have "flow0 x s ∉ interior M"
proof
assume interior: "flow0 x s ∈ interior M"
have "s ∈ existence_ivl0 x" using ivl_subset_existence_ivl[OF ‹t ∈ _›] s by auto
from flow_continuous[OF this, THEN isContD, THEN topological_tendstoD, OF open_interior interior]
have "∀⇩F s' in at s. flow0 x s' ∈ interior M" by auto
then have "∀⇩F s' in at_right s. flow0 x s' ∈ interior M"
by (auto simp: eventually_at_split)
moreover have "∀⇩F s' in at_right s. s' < t"
using tendsto_ident_at ‹s < t›
by (rule order_tendstoD)
ultimately have "∀⇩F s' in at_right s. flow0 x s' ∈ M ∧ s' < t"
by eventually_elim (use interior_subset[of M] in auto)
then obtain s' where s': "s < s'" "s' < t" "⋀y. y > s ⟹ y ≤ s' ⟹ flow0 x y ∈ M"
by (auto simp: eventually_at_right_field_le)
have s'_ivl: "flow0 x ` {0..s'} ⊆ M"
proof safe
fix s'' assume "s'' ∈ {0 .. s'}"
then show "flow0 x s'' ∈ M"
using s interior_subset[of M] s'
by (cases "s'' ≤ s") auto
qed
with s_max[of s'] ‹s' < t› ‹0 ≤ s› ‹s < s'› show False by auto
qed
then have "flow0 x s ∈ frontier M"
using s closure_subset[of M]
by (force simp: frontier_def)
moreover
have "compact (flow0 x -` M ∩ {s..t})" (is "compact ?C")
unfolding compact_eq_bounded_closed
proof
have "bounded {s .. t}" by simp
then show "bounded ?C"
by (rule bounded_subset) auto
show "closed ?C"
using ‹closed M› assms mem_existence_ivl_iv_defined(2)[OF t_ex] ivl_subset_existence_ivl[OF t_ex] ‹0 ≤ s›
by (intro closed_vimage_Int) (auto intro!: continuous_intros)
qed
have "∃⇩F s' in at_right s. flow0 x s' ∉ M"
apply (rule ccontr)
unfolding not_frequently
proof -
assume "∀⇩F s' in at_right s. ¬ flow0 x s' ∉ M"
moreover have "∀⇩F s' in at_right s. s' < t"
using tendsto_ident_at ‹s < t›
by (rule order_tendstoD)
ultimately have "∀⇩F s' in at_right s. flow0 x s' ∈ M ∧ s' < t" by eventually_elim auto
then obtain s' where s': "s < s'"
"⋀y. y > s ⟹ y < s' ⟹ flow0 x y ∈ M"
"⋀y. y > s ⟹ y < s' ⟹ y < t"
by (auto simp: eventually_at_right_field)
define s'' where "s'' = (s + s') / 2"
have "0 ≤ s''" "s'' ≤ t" "s < s''" "s'' < s'"
using s s'
by (auto simp del: divide_le_eq_numeral1 le_divide_eq_numeral1 simp: s''_def) fastforce
then have "flow0 x ` {0..s''} ⊆ M"
using s s'
apply auto
subgoal for u
by (cases "u≤s") auto
done
from s_max[OF ‹0 ≤ s''› ‹s''≤ t› this] ‹s'' > s›
show False by simp
qed
ultimately show ?thesis ..
qed
subsection ‹Connectedness›
lemma fcontX:
shows "continuous_on X f"
using auto_local_lipschitz local_lipschitz_continuous_on by blast
lemma fcontx:
assumes "x ∈ X"
shows "continuous (at x) f"
proof -
have "open X" by simp
from continuous_on_eq_continuous_at[OF this]
show ?thesis using fcontX assms(1) by blast
qed
lemma continuous_at_imp_cball:
assumes "continuous (at x) g"
assumes "g x > (0::real)"
obtains r where "r > 0" "∀y ∈ cball x r. g y > 0"
proof -
from assms(1)
obtain d where "d>0" "g ` (ball x d) ⊆ ball (g x) ((g x)/2)"
by (meson assms(2) continuous_at_ball half_gt_zero)
then have "∀y ∈ cball x (d/2). g y > 0"
by (smt assms(2) dist_norm image_subset_iff mem_ball mem_cball pos_half_less real_norm_def)
thus ?thesis
using ‹0 < d› that half_gt_zero by blast
qed
text ‹ ‹flow0› is ‹path_connected› ›
lemma flow0_path_connected_time:
assumes "ts ⊆ existence_ivl0 x" "path_connected ts"
shows "path_connected (flow0 x ` ts)"
proof -
have "continuous_on ts (flow0 x)"
by (meson assms continuous_on_sequentially flow_continuous_on subsetD)
from path_connected_continuous_image[OF this assms(2)]
show ?thesis .
qed
lemma flow0_path_connected:
assumes "path_connected D"
"path_connected ts"
"⋀x. x ∈ D ⟹ ts ⊆ existence_ivl0 x"
shows "path_connected ( (λ(x, y). flow0 x y) ` (D × ts))"
proof -
have "D × ts ⊆ Sigma X existence_ivl0"
using assms(3) subset_iff by fastforce
then have a1:"continuous_on (D × ts) (λ(x, y). flow0 x y)"
using flow_continuous_on_state_space continuous_on_subset by blast
have a2 : "path_connected (D × ts)" using path_connected_Times assms by auto
from path_connected_continuous_image[OF a1 a2]
show ?thesis .
qed
end
subsection ‹Return Time and Implicit Function Theorem›
context c1_on_open_euclidean begin
lemma flow_implicit_function:
fixes s::"'a::euclidean_space ⇒ real" and S::"'a set"
assumes t: "t ∈ existence_ivl0 x" and x: "x ∈ X" and st: "s (flow0 x t) = 0"
assumes Ds: "⋀x. (s has_derivative blinfun_apply (Ds x)) (at x)"
assumes DsC: "isCont Ds (flow0 x t)"
assumes nz: "Ds (flow0 x t) (f (flow0 x t)) ≠ 0"
obtains u e
where "s (flow0 x (u x)) = 0"
"u x = t"
"(⋀y. y ∈ cball x e ⟹ s (flow0 y (u y)) = 0)"
"continuous_on (cball x e) u"
"(λt. (t, u t)) ` cball x e ⊆ Sigma X existence_ivl0"
"0 < e" "(u has_derivative (- blinfun_scaleR_left
(inverse (blinfun_apply (Ds (flow0 x t)) (f (flow0 x t)))) o⇩L
(Ds (flow0 x t) o⇩L flowderiv x t) o⇩L embed1_blinfun)) (at x)"
proof -
note [derivative_intros] = has_derivative_compose[OF _ Ds]
have cont_s: "continuous_on UNIV s" by (rule has_derivative_continuous_on[OF Ds])
note cls[simp, intro] = closed_levelset[OF cont_s]
then have xt1: "(x, t) ∈ Sigma X existence_ivl0"
by (auto simp: t x)
have D: "(⋀x. x ∈ Sigma X existence_ivl0 ⟹
((λ(x, t). s (flow0 x t)) has_derivative
blinfun_apply (Ds (flow0 (fst x) (snd x)) o⇩L (flowderiv (fst x) (snd x))))
(at x))"
by (auto intro!: derivative_eq_intros)
have C: "isCont (λx. Ds (flow0 (fst x) (snd x)) o⇩L flowderiv (fst x) (snd x))
(x, t)"
using flowderiv_continuous_on[unfolded continuous_on_eq_continuous_within,
rule_format, OF xt1]
using at_within_open[OF xt1 open_state_space]
by (auto intro!: continuous_intros tendsto_eq_intros x t
isCont_tendsto_compose[OF DsC, unfolded poincare_map_def]
simp: split_beta' isCont_def)
have Z: "(case (x, t) of (x, t) ⇒ s (flow0 x t)) = 0"
by (auto simp: st)
have I1: "blinfun_scaleR_left (inverse (Ds (flow0 x t)(f (flow0 x t)))) o⇩L
((Ds (flow0 (fst (x, t))
(snd (x, t))) o⇩L
flowderiv (fst (x, t))
(snd (x, t))) o⇩L
embed2_blinfun)
= 1⇩L"
using nz
by (auto intro!: blinfun_eqI
simp: flowderiv_def blinfun.bilinear_simps inverse_eq_divide poincare_map_def)
have I2: "((Ds (flow0 (fst (x, t))
(snd (x, t))) o⇩L
flowderiv (fst (x, t))
(snd (x, t))) o⇩L
embed2_blinfun) o⇩L blinfun_scaleR_left (inverse (Ds (flow0 x t)(f (flow0 x t))))
= 1⇩L"
using nz
by (auto intro!: blinfun_eqI
simp: flowderiv_def blinfun.bilinear_simps inverse_eq_divide poincare_map_def)
show ?thesis
apply (rule implicit_function_theorem[where f="λ(x, t). s (flow0 x t)"
and S="Sigma X existence_ivl0", OF D xt1 open_state_space order_refl C Z I1 I2])
apply blast
unfolding split_beta' fst_conv snd_conv poincare_map_def[symmetric]
..
qed
lemma flow_implicit_function_at:
fixes s::"'a::euclidean_space ⇒ real" and S::"'a set"
assumes x: "x ∈ X" and st: "s x = 0"
assumes Ds: "⋀x. (s has_derivative blinfun_apply (Ds x)) (at x)"
assumes DsC: "isCont Ds x"
assumes nz: "Ds x (f x) ≠ 0"
assumes pos: "e > 0"
obtains u d
where
"0 < d"
"u x = 0"
"⋀y. y ∈ cball x d ⟹ s (flow0 y (u y)) = 0"
"⋀y. y ∈ cball x d ⟹ ¦u y¦ < e"
"⋀y. y ∈ cball x d ⟹ u y ∈ existence_ivl0 y"
"continuous_on (cball x d) u"
"(u has_derivative -Ds x /⇩R (Ds x) (f x)) (at x)"
proof -
have x0: "flow0 x 0 = x" by (simp add: x)
from flow_implicit_function[OF existence_ivl_zero[OF x] x, unfolded x0, of s, OF st Ds DsC nz]
obtain u d0 where
s0: "s (flow0 x (u x)) = 0"
and u0: "u x = 0"
and u: "⋀y. y ∈ cball x d0 ⟹ s (flow0 y (u y)) = 0"
and uc: "continuous_on (cball x d0) u"
and uex: "(λt. (t, u t)) ` cball x d0 ⊆ Sigma X existence_ivl0"
and d0: "0 < d0"
and u': "(u has_derivative
blinfun_apply
(- blinfun_scaleR_left (inverse (blinfun_apply (Ds x) (f x))) o⇩L (Ds x o⇩L flowderiv x 0) o⇩L embed1_blinfun))
(at x)"
by blast
have "at x within cball x d0 = at x" by (rule at_within_interior) (auto simp: ‹0 < d0›)
then have "(u ⤏ 0) (at x)"
using uc d0 by (auto simp: continuous_on_def u0 dest!: bspec[where x=x])
from tendstoD[OF this ‹0 < e›] pos u0
obtain d1 where d1: "0 < d1" "⋀xa. dist xa x ≤ d1 ⟹ ¦u xa¦ < e"
unfolding eventually_at_le
by force
define d where "d = min d0 d1"
have "0 < d" by (auto simp: d_def d0 d1)
moreover note u0
moreover have "⋀y. y ∈ cball x d ⟹ s (flow0 y (u y)) = 0" by (auto intro!: u simp: d_def)
moreover have "⋀y. y ∈ cball x d ⟹ ¦u y¦ < e" using d1 by (auto simp: d_def dist_commute)
moreover have "⋀y. y ∈ cball x d ⟹ u y ∈ existence_ivl0 y"
using uex by (force simp: d_def)
moreover have "continuous_on (cball x d) u"
using uc by (rule continuous_on_subset) (auto simp: d_def)
moreover
have "(u has_derivative -Ds x /⇩R (Ds x) (f x)) (at x)"
using u'
by (rule has_derivative_subst) (auto intro!: ext simp: x x0 flowderiv_def blinfun.bilinear_simps)
ultimately show ?thesis ..
qed
lemma returns_to_implicit_function_gen:
fixes s::"'a::euclidean_space ⇒ real"
assumes rt: "returns_to {x ∈ S. s x = 0} x" (is "returns_to ?P x")
assumes cS: "closed S"
assumes Ds: "⋀x. (s has_derivative blinfun_apply (Ds x)) (at x)"
"isCont Ds (poincare_map ?P x)"
"Ds (poincare_map ?P x) (f (poincare_map ?P x)) ≠ 0"
obtains u e
where "s (flow0 x (u x)) = 0"
"u x = return_time ?P x"
"(⋀y. y ∈ cball x e ⟹ s (flow0 y (u y)) = 0)"
"continuous_on (cball x e) u"
"(λt. (t, u t)) ` cball x e ⊆ Sigma X existence_ivl0"
"0 < e" "(u has_derivative (- blinfun_scaleR_left
(inverse (blinfun_apply (Ds (poincare_map ?P x)) (f (poincare_map ?P x)))) o⇩L
(Ds (poincare_map ?P x) o⇩L flowderiv x (return_time ?P x)) o⇩L embed1_blinfun)) (at x)"
proof -
note [derivative_intros] = has_derivative_compose[OF _ Ds(1)]
have cont_s: "continuous_on UNIV s" by (rule has_derivative_continuous_on[OF Ds(1)])
note cls[simp, intro] = closed_levelset[OF cont_s]
let ?t1 = "return_time ?P x"
have cls[simp, intro]: "closed {x ∈ S. s x = 0}"
by (rule closed_levelset_within) (auto intro!: cS continuous_on_subset[OF cont_s])
have *: "poincare_map ?P x = flow0 x (return_time {x ∈ S. s x = 0} x)"
by (simp add: poincare_map_def)
have "return_time {x ∈ S. s x = 0} x ∈ existence_ivl0 x"
"x ∈ X"
"s (poincare_map ?P x) = 0"
using poincare_map_returns rt
by (auto intro!: return_time_exivl rt)
note E = flow_implicit_function[of "return_time ?P x" x s Ds, OF this[unfolded *] Ds[unfolded *],
folded *]
show ?thesis
by (rule E) rule
qed
text ‹c.f. Perko Section 3.7 Lemma 2 part 1.›
lemma flow_transversal_surface_finite_intersections:
fixes s::"'a ⇒ 'b::real_normed_vector"
and Ds::"'a ⇒ 'a ⇒⇩L 'b"
assumes "closed S"
assumes "⋀x. (s has_derivative (Ds x)) (at x)"
assumes "⋀x. x ∈ S ⟹ s x = 0 ⟹ Ds x (f x) ≠ 0"
assumes "a ≤ b" "{a .. b} ⊆ existence_ivl0 x"
shows "finite {t∈{a..b}. flow0 x t ∈ {x ∈ S. s x = 0}}"
proof cases
note Ds = ‹⋀x. (s has_derivative (Ds x)) (at x)›
note transversal = ‹⋀x. x ∈ S ⟹ s x = 0 ⟹ Ds x (f x) ≠ 0›
assume "a < b"
show ?thesis
proof (rule ccontr)
let ?S = "{x ∈ S. s x = 0}"
let ?T = "{t∈{a..b}. flow0 x t ∈ {x ∈ S. s x = 0}}"
define φ where "φ = flow0 x"
have [THEN continuous_on_compose2, continuous_intros]: "continuous_on S s"
by (auto simp: intro!: has_derivative_continuous_on Ds intro: has_derivative_at_withinI)
assume "infinite ?T"
from compact_sequentialE[OF compact_Icc[of a b] this]
obtain t tl where t: "t n ∈ ?T" "flow0 x (t n) ∈ ?S" "t n ∈ {a .. b}" "t n ≠ tl"
and tl: "t ⇢ tl" "tl ∈ {a..b}"
for n
by force
have tl_ex: "tl ∈ existence_ivl0 x" using ‹{a .. b} ⊆ existence_ivl0 x› ‹tl ∈ {a .. b}› by auto
have "closed ?S"
by (auto intro!: closed_levelset_within ‹closed S› continuous_intros)
moreover
have "∀n. flow0 x (t n) ∈ ?S"
using t by auto
moreover
have flow_t: "(λn. flow0 x (t n)) ⇢ flow0 x tl"
by (auto intro!: tendsto_eq_intros tl_ex tl)
ultimately have "flow0 x tl ∈ ?S"
by (metis (no_types, lifting) closed_sequentially)
let ?qt = "λt. (flow0 x t - flow0 x tl) /⇩R (t - tl)"
from flow_has_vector_derivative[OF tl_ex, THEN has_vector_derivative_withinD]
have qt_tendsto: "?qt ─tl→ f (flow0 x tl)" .
let ?q = "λn. ?qt (t n)"
have "filterlim t (at tl) sequentially"
using tl(1)
by (rule filterlim_atI) (simp add: t)
with qt_tendsto have "?q ⇢ f (flow0 x tl)"
by (rule filterlim_compose)
then have "((λn. Ds (flow0 x tl) (?q n))) ⇢ Ds (flow0 x tl) (f (flow0 x tl))"
by (auto intro!: tendsto_intros)
moreover
from flow_lipschitzE[OF ‹{a .. b} ⊆ existence_ivl0 x›] obtain L' where L': "L'-lipschitz_on {a..b} (flow0 x)" .
define L where "L = L' + 1"
from lipschitz_on_le[OF L', of L] lipschitz_on_nonneg[OF L']
have L: "L-lipschitz_on {a .. b} (flow0 x)" and "L > 0"
by (auto simp: L_def)
from flow_lipschitzE[OF ‹{a .. b} ⊆ existence_ivl0 x›] obtain L' where "L'-lipschitz_on {a..b} (flow0 x)" .
have s[simp]: "s (flow0 x (t n)) = 0""s (flow0 x tl) = 0"
for n
using t ‹flow0 x tl ∈ ?S›
by auto
from Ds(1)[of "flow0 x tl", unfolded has_derivative_within]
have "(λy. (1 / norm (y - flow0 x tl)) *⇩R (s y - (s (flow0 x tl) + blinfun_apply (Ds (flow0 x tl)) (y - flow0 x tl)))) ─flow0 x tl→ 0"
by auto
then have "((λy. (1 / norm (y - flow0 x tl)) *⇩R (s y - (s (flow0 x tl) + blinfun_apply (Ds (flow0 x tl)) (y - flow0 x tl)))) ⤏ 0)
(nhds (flow0 x tl))"
by (rule tendsto_nhds_continuousI) simp
from filterlim_compose[OF this flow_t]
have "(λxa. (blinfun_apply (Ds (flow0 x tl)) (flow0 x (t xa) - flow0 x tl)) /⇩R norm (flow0 x (t xa) - flow0 x tl))
⇢ 0"
using t
by (auto simp: inverse_eq_divide tendsto_minus_cancel_right)
from tendsto_mult[OF tendsto_const[of "L"] tendsto_norm[OF this, simplified, simplified divide_inverse_commute[symmetric]]]
have Ds0: "(λxa. norm (blinfun_apply (Ds (flow0 x tl)) (flow0 x (t xa) - flow0 x tl)) / (norm (flow0 x (t xa) - flow0 x tl)/(L))) ⇢ 0"
by (auto simp: ac_simps)
from _ Ds0 have "((λn. Ds (flow0 x tl) (?q n)) ⇢ 0)"
apply (rule Lim_null_comparison)
apply (rule eventuallyI)
unfolding norm_scaleR blinfun.scaleR_right abs_inverse divide_inverse_commute[symmetric]
subgoal for n
apply (cases "flow0 x (t n) = flow0 x tl")
subgoal by (simp add: blinfun.bilinear_simps)
subgoal
apply (rule divide_left_mono)
using lipschitz_onD[OF L, of "t n" tl] ‹0 < L› t(3) tl(2)
by (auto simp: algebra_split_simps zero_less_divide_iff dist_norm pos_divide_le_eq
intro!: add_pos_nonneg)
done
done
ultimately have "Ds (flow0 x tl) (f (flow0 x tl)) = 0"
by (rule LIMSEQ_unique)
moreover have "Ds (flow0 x tl) (f (flow0 x tl)) ≠ 0"
by (rule transversal) (use ‹flow0 x tl ∈ ?S› in auto)
ultimately show False by auto
qed
qed (use assms in auto)
lemma uniform_limit_flow0_state:
assumes "compact C"
assumes "C ⊆ X"
shows "uniform_limit C (λs x. flow0 x s) (λx. flow0 x 0) (at 0)"
proof (cases "C = {}")
case True then show ?thesis by auto
next
case False show ?thesis
proof (rule uniform_limitI)
fix e::real assume "0 < e"
{
fix x assume "x ∈ C"
with assms have "x ∈ X" by auto
from existence_ivl_cballs[OF UNIV_I ‹x ∈ X›]
obtain t L u where "⋀y. y ∈ cball x u ⟹ cball 0 t ⊆ existence_ivl0 y"
"⋀s y. y ∈ cball x u ⟹ s ∈ cball 0 t ⟹ flow0 y s ∈ cball y u"
"L-lipschitz_on (cball 0 t×cball x u) (λ(t, x). flow0 x t)"
"⋀y. y ∈ cball x u ⟹ cball y u ⊆ X"
"0 < t" "0 < u"
by metis
then have "∃L. ∃u>0. ∃t>0. L-lipschitz_on (cball 0 t×cball x u) (λ(t, x). flow0 x t)" by blast
} then have "∀x∈C. ∃L. ∃u>0. ∃t>0. L-lipschitz_on (cball 0 t×cball x u) (λ(t, x). flow0 x t)" ..
then obtain L d' u' where
L: "⋀x. x ∈ C ⟹ (L x)-lipschitz_on (cball 0 (d' x)×cball x (u' x)) (λ(t, x). flow0 x t)"
and d': "⋀x. x ∈ C ⟹ d' x > 0"
and u': "⋀x. x ∈ C ⟹ u' x > 0"
by metis
have "C ⊆ (⋃c∈C. ball c (u' c))" using u' by auto
from compactE_image[OF ‹compact C› _ this]
obtain C' where "C' ⊆ C" and [simp]: "finite C'" and C'_cover: "C ⊆ (⋃c∈C'. ball c (u' c))"
by auto
from C'_cover obtain c' where c': "x ∈ C ⟹ x ∈ ball (c' x) (u' (c' x))" "x ∈ C ⟹ c' x ∈ C'" for x
by (auto simp: subset_iff) metis
have "∀⇩F s in at 0. ∀x∈ball c (u' c). dist (flow0 x s) (flow0 x 0) < e" if "c ∈ C'" for c
proof -
have cC: "c ∈ C"
using c' ‹c ∈ C'› d' ‹C' ⊆ C›
by auto
have *: "dist (flow0 x s) (flow0 x 0) ≤ L c * ¦s¦"
if "x∈ball c (u' c)"
"s ∈ cball 0 (d' c)"
for x s
proof -
from L[OF cC, THEN lipschitz_onD, of "(0, x)" "(s, x)"] d'[OF cC] that
show ?thesis
by (auto simp: dist_prod_def dist_commute)
qed
have "∀⇩F s in at 0. abs s < d' c"
by (rule order_tendstoD tendsto_intros)+ (use d' cC in auto)
moreover have "∀⇩F s in at 0. L c * ¦s¦ < e"
by (rule order_tendstoD tendsto_intros)+ (use ‹0 < e› in auto)
ultimately show ?thesis
apply eventually_elim
apply (use * in auto)
by smt
qed
then have "∀⇩F s in at 0. ∀c∈C'. ∀x∈ball c (u' c). dist (flow0 x s) (flow0 x 0) < e"
by (simp add: eventually_ball_finite_distrib)
then show "∀⇩F s in at 0. ∀x∈C. dist (flow0 x s) (flow0 x 0) < e"
apply eventually_elim
apply auto
subgoal for s x
apply (drule bspec[where x="c' x"])
apply (simp add: c'(2))
apply (drule bspec) prefer 2 apply assumption
apply auto
using c'(1) by auto
done
qed
qed
end
subsection ‹Fixpoints›
context auto_ll_on_open begin
lemma fixpoint_sol:
assumes "x ∈ X" "f x = 0"
shows "existence_ivl0 x = UNIV" "flow0 x t = x"
proof -
have sol: "((λt::real. x) solves_ode (λ_. f)) UNIV X"
apply (rule solves_odeI)
by(auto simp add: assms intro!: derivative_intros)
from maximal_existence_flow[OF sol] have
"UNIV ⊆ existence_ivl0 x" "flow0 x t = x" by auto
thus "existence_ivl0 x = UNIV" "flow0 x t = x" by auto
qed
end
end