diff --git a/thys/Poincare_Bendixson/Affine_Arithmetic_Misc.thy b/thys/Poincare_Bendixson/Affine_Arithmetic_Misc.thy --- a/thys/Poincare_Bendixson/Affine_Arithmetic_Misc.thy +++ b/thys/Poincare_Bendixson/Affine_Arithmetic_Misc.thy @@ -1,148 +1,147 @@ theory Affine_Arithmetic_Misc imports "HOL-ODE-Numerics.ODE_Numerics" begin - section \Branch-And-Bound Arithmetic\ primrec prove_nonneg::"(nat * nat * string) list \ nat \ nat \ slp \ real aform list list \ bool" where "prove_nonneg prnt 0 p slp X = (let _ = if prnt \ [] then print (STR ''# depth limit exceeded\'') else () in False)" | "prove_nonneg prnt (Suc i) p slp XXS = (case XXS of [] \ True | (X#XS) \ let RS = approx_slp_outer p 1 slp X in if RS\None \ Inf_aform' p (hd (the RS)) \ 0 then let _ = if prnt \ [] then print (STR ''# Success\'') else (); _ = if prnt \ [] then print (String.implode ((shows ''# '' o shows_box_of_aforms_hr X) ''\'')) else (); _ = fold (\(a, b, c) _. print (String.implode (shows_segments_of_aform a b X c ''\''))) prnt () in prove_nonneg prnt i p slp XS else let _ = if prnt \ [] then print (STR ''# Split\'') else () in case split_aforms_largest_uncond X of (a, b) \ prove_nonneg prnt i p slp (a#b#XS))" lemma prove_nonneg_simps[simp]: "prove_nonneg prnt 0 p slp X = False" "prove_nonneg prnt (Suc i) p slp XXS = (case XXS of [] \ True | (X#XS) \ let RS = approx_slp_outer p 1 slp X in if RS\None \ Inf_aform' p (hd (the RS)) \ 0 then prove_nonneg prnt i p slp XS else case split_aforms_largest_uncond X of (a, b) \ prove_nonneg prnt i p slp (a#b#XS))" by (auto simp: Let_def split: if_splits option.splits list.splits) lemmas [simp del] = prove_nonneg.simps lemma split_aforms_lemma: fixes xs::"real list" assumes "split_aforms XS i = (YS, ZS)" assumes "xs \ Joints XS" shows "xs \ Joints YS \ Joints ZS" using set_rev_mp[OF assms(2) Joints_map_split_aform[of XS i]] assms(1) by (auto simp: split_aforms_def o_def) lemma prove_nonneg_empty[simp]: "prove_nonneg prnt (Suc i) p slp []" by simp lemma prove_nonneg_fuel_mono: "prove_nonneg prnt (Suc i) p (slp_of_fas [fa]) YSS" if "prove_nonneg prnt i p (slp_of_fas [fa]) YSS" using that proof (induction i arbitrary: YSS) case 0 then show ?case by simp next case (Suc i) from Suc.prems show ?case supply [simp del] = prove_nonneg_simps apply (subst prove_nonneg_simps) apply (auto simp: Let_def split: if_splits option.splits list.splits) subgoal apply (rule Suc.IH) apply (subst (asm) prove_nonneg_simps) by (auto simp: Let_def split: if_splits option.splits list.splits) subgoal apply (rule Suc.IH) apply (subst (asm) prove_nonneg.simps) by (auto simp: Let_def split: if_splits option.splits list.splits) subgoal apply (rule Suc.IH) apply (subst (asm) prove_nonneg.simps) by (auto simp: Let_def split: if_splits option.splits list.splits) done qed lemma prove_nonneg_mono: "prove_nonneg prnt i p (slp_of_fas [fa]) YSS" if "prove_nonneg prnt i p (slp_of_fas [fa]) (YS # YSS)" using that proof (induction i arbitrary: YS YSS) case 0 then show ?case by auto next case (Suc i) from Suc.prems show ?case supply [simp del] = prove_nonneg_simps apply (subst (asm) prove_nonneg_simps) apply (auto simp: Let_def split: if_splits option.splits list.splits) subgoal by (rule prove_nonneg_fuel_mono) subgoal for x y apply (rule prove_nonneg_fuel_mono) apply (rule Suc.IH[of y]) by (rule Suc.IH[of x]) subgoal for x y apply (rule prove_nonneg_fuel_mono) apply (rule Suc.IH[of y]) by (rule Suc.IH[of x]) done qed lemma prove_nonneg: assumes "prove_nonneg prnt i p (slp_of_fas [fa]) XSS" shows "\XS \ set XSS. \xs \ Joints XS. interpret_floatarith fa xs \ 0" using assms proof (induction i arbitrary: XSS) case 0 then show ?case by (auto ) next case (Suc i) show ?case proof (cases XSS) case Nil then show ?thesis by auto next case (Cons YS YSS) show ?thesis unfolding Cons apply auto subgoal for xs using Suc.prems apply (auto simp: Cons Let_def split: if_splits option.splits) subgoal for ys apply (drule approx_slp_outer_plain) apply (rule refl) apply force apply assumption apply simp apply (frule Joints_imp_length_eq[where XS=ys]) apply (auto simp: Suc_length_conv) by (smt Inf_aform'_Affine_le) subgoal apply (simp add: split_aforms_largest_uncond_def split: prod.splits) apply (drule Suc.IH) apply (drule split_aforms_lemma, assumption) by auto subgoal apply (simp add: split_aforms_largest_uncond_def split: prod.splits) apply (drule Suc.IH) apply (drule split_aforms_lemma, assumption) by auto done subgoal for XS xs using Suc.prems apply (auto simp: Cons Let_def split: if_splits option.splits) subgoal for ys by (rule Suc.IH[rule_format], assumption, assumption, assumption) subgoal for ys apply (drule prove_nonneg_mono) apply (drule prove_nonneg_mono) by (rule Suc.IH[rule_format], assumption, assumption, assumption) subgoal for ys apply (drule prove_nonneg_mono) apply (drule prove_nonneg_mono) by (rule Suc.IH[rule_format], assumption, assumption, assumption) done done qed qed end \ No newline at end of file diff --git a/thys/Poincare_Bendixson/Analysis_Misc.thy b/thys/Poincare_Bendixson/Analysis_Misc.thy --- a/thys/Poincare_Bendixson/Analysis_Misc.thy +++ b/thys/Poincare_Bendixson/Analysis_Misc.thy @@ -1,1134 +1,1135 @@ section \Additions to HOL-Analysis\ theory Analysis_Misc imports Ordinary_Differential_Equations.ODE_Analysis begin subsection \Unsorted Lemmas (TODO: sort!)\ lemma uminus_uminus_image: "uminus ` uminus ` S = S" for S::"'r::ab_group_add set" by (auto simp: image_image) lemma in_uminus_image_iff[simp]: "x \ uminus ` S \ - x \ S" for S::"'r::ab_group_add set" by force lemma closed_subsegmentI: "w + t *\<^sub>R (z - w) \ {x--y}" if "w \ {x -- y}" "z \ {x -- y}" and t: "0 \ t" "t\ 1" proof - from that obtain u v where w_def: "w = (1 - u) *\<^sub>R x + u *\<^sub>R y" and u: "0 \ u" "u \ 1" and z_def: "z = (1 - v) *\<^sub>R x + v *\<^sub>R y" and v: "0 \ v" "v \ 1" by (auto simp: in_segment) have "w + t *\<^sub>R (z - w) = (1 - (u - t * (u - v))) *\<^sub>R x + (u - t * (u - v)) *\<^sub>R y" by (simp add: algebra_simps w_def z_def) also have "\ \ {x -- y}" - apply (rule closed_segmentI[OF _ refl]) - using t u v + unfolding closed_segment_image_interval + apply (rule imageI) + using t u v apply auto apply (metis (full_types) diff_0_right diff_left_mono linear mult_left_le_one_le mult_nonneg_nonpos order.trans) by (smt mult_left_le_one_le mult_nonneg_nonneg vector_space_over_itself.scale_right_diff_distrib) finally show ?thesis . qed lemma tendsto_minus_cancel_right: "((\x. -g x) \ l) F \ (g \ -l) F" \ \cf @{thm tendsto_minus_cancel_left}\ for g::"_ \ 'b::topological_group_add" by (simp add: tendsto_minus_cancel_left) lemma tendsto_nhds_continuousI: "(f \ l) (nhds x)" if "(f \ l) (at x)" "f x = l" \ \TODO: the assumption is continuity of f at x\ proof (rule topological_tendstoI) fix S::"'b set" assume "open S" "l \ S" from topological_tendstoD[OF that(1) this] have "\\<^sub>F x in at x. f x \ S" . then show "\\<^sub>F x in nhds x. f x \ S" unfolding eventually_at_filter by eventually_elim (auto simp: that \l \ S\) qed lemma inj_composeD: assumes "inj (\x. g (t x))" shows "inj t" using assms by (auto simp: inj_def) lemma compact_sequentialE: fixes S T::"'a::first_countable_topology set" assumes "compact S" assumes "infinite T" assumes "T \ S" obtains t::"nat \ 'a" and l::'a where "\n. t n \ T" "\n. t n \ l" "t \ l" "l \ S" proof - from Heine_Borel_imp_Bolzano_Weierstrass[OF assms] obtain l where "l \ S" "l islimpt T" by metis then obtain t where "t n \ T" "t n \ l" "t \ l" "l \ S" for n unfolding islimpt_sequential by auto then show ?thesis .. qed lemma infinite_countable_subsetE: fixes S::"'a set" assumes "infinite S" obtains g::"nat\'a" where "inj g" "range g \ S" using assms by atomize_elim (simp add: infinite_countable_subset) lemma real_quad_ge: "2 * (an * bn) \ an * an + bn * bn" for an bn::real by (sos "(((A<0 * R<1) + (R<1 * (R<1 * [an + ~1*bn]^2))))") lemma inner_quad_ge: "2 * (a \ b) \ a \ a + b \ b" for a b::"'a::euclidean_space"\ \generalize?\ proof - show ?thesis by (subst (1 2 3) euclidean_inner) (auto simp add: sum.distrib[symmetric] sum_distrib_left intro!: sum_mono real_quad_ge) qed lemma inner_quad_gt: "2 * (a \ b) < a \ a + b \ b" if "a \ b" for a b::"'a::euclidean_space"\ \generalize?\ proof - from that obtain i where "i \ Basis" "a \ i \ b \ i" by (auto simp: euclidean_eq_iff[where 'a='a]) then have "2 * (a \ i * (b \ i)) < a \ i * (a \ i) + b \ i * (b \ i)" using sum_sqs_eq[of "a\i" "b\i"] by (auto intro!: le_neq_trans real_quad_ge) then show ?thesis by (subst (1 2 3) euclidean_inner) (auto simp add: \i \ Basis\ sum.distrib[symmetric] sum_distrib_left intro!: sum_strict_mono_ex1 real_quad_ge) qed lemma closed_segment_line_hyperplanes: "{a -- b} = range (\u. a + u *\<^sub>R (b - a)) \ {x. a \ (b - a) \ x \ (b - a) \ x \ (b - a) \ b \ (b - a)}" if "a \ b" for a b::"'a::euclidean_space" proof safe fix x assume x: "x \ {a--b}" then obtain u where u: "0 \ u" "u \ 1" and x_eq: "x = a + u *\<^sub>R (b - a)" by (auto simp add: in_segment algebra_simps) show "x \ range (\u. a + u *\<^sub>R (b - a))" using x_eq by auto have "2 * (a \ b) \ a \ a + b \ b" by (rule inner_quad_ge) then have "u * (2 * (a \ b) - a \ a - b \ b) \ 0" "0 \ (1 - u) * (a \ a + b \ b - a \ b * 2)" by (simp_all add: mult_le_0_iff u) then show " a \ (b - a) \ x \ (b - a)" "x \ (b - a) \ b \ (b - a)" by (auto simp: x_eq algebra_simps power2_eq_square inner_commute) next fix u assume "a \ (b - a) \ (a + u *\<^sub>R (b - a)) \ (b - a)" "(a + u *\<^sub>R (b - a)) \ (b - a) \ b \ (b - a)" then have "0 \ u * ((b - a) \ (b - a))" "0 \ (1 - u) * ((b - a) \ (b - a))" by (auto simp: algebra_simps) then have "0 \ u" "u \ 1" using inner_ge_zero[of "(b - a)"] that by (auto simp add: zero_le_mult_iff) then show "a + u *\<^sub>R (b - a) \ {a--b}" by (auto simp: in_segment algebra_simps) qed lemma open_segment_line_hyperplanes: "{a <--< b} = range (\u. a + u *\<^sub>R (b - a)) \ {x. a \ (b - a) < x \ (b - a) \ x \ (b - a) < b \ (b - a)}" if "a \ b" for a b::"'a::euclidean_space" proof safe fix x assume x: "x \ {a<--R (b - a)" by (auto simp add: in_segment algebra_simps) show "x \ range (\u. a + u *\<^sub>R (b - a))" using x_eq by auto have "2 * (a \ b) < a \ a + b \ b" using that by (rule inner_quad_gt) then have "u * (2 * (a \ b) - a \ a - b \ b) < 0" "0 < (1 - u) * (a \ a + b \ b - a \ b * 2)" by (simp_all add: mult_less_0_iff u) then show " a \ (b - a) < x \ (b - a)" "x \ (b - a) < b \ (b - a)" by (auto simp: x_eq algebra_simps power2_eq_square inner_commute) next fix u assume "a \ (b - a) < (a + u *\<^sub>R (b - a)) \ (b - a)" "(a + u *\<^sub>R (b - a)) \ (b - a) < b \ (b - a)" then have "0 < u * ((b - a) \ (b - a))" "0 < (1 - u) * ((b - a) \ (b - a))" by (auto simp: algebra_simps) then have "0 < u" "u < 1" using inner_ge_zero[of "(b - a)"] that by (auto simp add: zero_less_mult_iff) then show "a + u *\<^sub>R (b - a) \ {a<-- x \ interior S \ at x within S = at x" by (auto intro: at_within_interior) lemma tendsto_at_topI: "(f \ l) at_top" if "\e. 0 < e \ \x0. \x\x0. dist (f x) l < e" for f::"'a::linorder_topology \ 'b::metric_space" using that apply (intro tendstoI) unfolding eventually_at_top_linorder by auto lemma tendsto_at_topE: fixes f::"'a::linorder_topology \ 'b::metric_space" assumes "(f \ l) at_top" assumes "e > 0" obtains x0 where "\x. x \ x0 \ dist (f x) l < e" proof - from assms(1)[THEN tendstoD, OF assms(2)] have "\\<^sub>F x in at_top. dist (f x) l < e" . then show ?thesis unfolding eventually_at_top_linorder by (auto intro: that) qed lemma tendsto_at_top_iff: "(f \ l) at_top \ (\e>0. \x0. \x\x0. dist (f x) l < e)" for f::"'a::linorder_topology \ 'b::metric_space" by (auto intro!: tendsto_at_topI elim!: tendsto_at_topE) lemma tendsto_at_top_eq_left: fixes f g::"'a::linorder_topology \ 'b::metric_space" assumes "(f \ l) at_top" assumes "\x. x \ x0 \ f x = g x" shows "(g \ l) at_top" unfolding tendsto_at_top_iff by (metis (no_types, hide_lams) assms(1) assms(2) linear order_trans tendsto_at_topE) lemma lim_divide_n: "(\x. e / real x) \ 0" proof - have "(\x. e * inverse (real x)) \ 0" by (auto intro: tendsto_eq_intros lim_inverse_n) then show ?thesis by (simp add: inverse_eq_divide) qed definition at_top_within :: "('a::order) set \ 'a filter" where "at_top_within s = (INF k \ s. principal ({k ..} \ s)) " lemma at_top_within_at_top[simp]: shows "at_top_within UNIV = at_top" unfolding at_top_within_def at_top_def by (auto) lemma at_top_within_empty[simp]: shows "at_top_within {} = top" unfolding at_top_within_def by (auto) definition "nhds_set X = (INF S\{S. open S \ X \ S}. principal S)" lemma eventually_nhds_set: "(\\<^sub>F x in nhds_set X. P x) \ (\S. open S \ X \ S \ (\x\S. P x))" unfolding nhds_set_def by (subst eventually_INF_base) (auto simp: eventually_principal) term "filterlim f (nhds_set (frontier X)) F" \ \f tends to the boundary of X?\ text \somewhat inspired by @{thm islimpt_range_imp_convergent_subsequence} and its dependencies. The class constraints seem somewhat arbitrary, perhaps this can be generalized in some way. \ lemma limpt_closed_imp_exploding_subsequence:\\TODO: improve name?!\ fixes f::"'a::{heine_borel,real_normed_vector} \ 'b::{first_countable_topology, t2_space}" assumes cont[THEN continuous_on_compose2, continuous_intros]: "continuous_on T f" assumes closed: "closed T" assumes bound: "\t. t \ T \ f t \ l" assumes limpt: "l islimpt (f ` T)" obtains s where "(f \ s) \ l" "\i. s i \ T" "\C. compact C \ C \ T \ \\<^sub>F i in sequentially. s i \ C" proof - from countable_basis_at_decseq[of l] obtain A where A: "\i. open (A i)" "\i. l \ A i" and evA: "\S. open S \ l \ S \ eventually (\i. A i \ S) sequentially" by blast from closed_Union_compact_subsets[OF closed] obtain C where C: "(\n. compact (C n))" "(\n. C n \ T)" "(\n. C n \ C (Suc n))" "\ (range C) = T" and evC: "(\K. compact K \ K \ T \ \\<^sub>F i in sequentially. K \ C i)" by (metis eventually_sequentially) have AC: "l \ A i - f ` C i" "open (A i - f ` C i)" for i using C bound by (fastforce intro!: open_Diff A compact_imp_closed compact_continuous_image continuous_intros)+ from islimptE[OF limpt AC] have "\t\T. f t \ A i - f ` C i \ f t \ l" for i by blast then obtain t where t: "\i. t i \ T" "\i. f (t i) \ A i - f ` C i" "\i. f (t i) \ l" by metis have "(f o t) \ l" using t by (auto intro!: topological_tendstoI dest!: evA elim!: eventually_mono) moreover have "\i. t i \ T" by fact moreover have "\\<^sub>F i in sequentially. t i \ K" if "compact K" "K \ T" for K using evC[OF that] by eventually_elim (use t in auto) ultimately show ?thesis .. qed lemma Inf_islimpt: "bdd_below S \ Inf S \ S \ S \ {} \ Inf S islimpt S" for S::"real set" by (auto simp: islimpt_in_closure intro!: closure_contains_Inf) context linorder begin text \HOL-analysis doesn't seem to have these, maybe they were never needed. Some variants are around @{thm Int_atLeastAtMost}, but with old-style naming conventions. Change to the "modern" I.. convention there?\ lemma Int_Ico[simp]: shows "{a..} \ {b..} = {max a b ..}" by (auto) lemma Int_Ici_Ico[simp]: shows "{a..} \ {b.. {b..} = {max a b .. {c.. b \ a \ c \ a" unfolding atLeastLessThan_def by auto lemma Ico_subset_Ioo_iff[simp]: "{a.. {c<.. b \ a \ c < a" unfolding greaterThanLessThan_def atLeastLessThan_def by auto lemma Icc_Un_Ici[simp]: shows "{a..b} \ {b..} = {min a b..}" unfolding atLeastAtMost_def atLeast_def atMost_def min_def by auto end lemma at_top_within_at_top_unbounded_right: fixes a::"'a::linorder" shows "at_top_within {a..} = at_top" unfolding at_top_within_def at_top_def apply (auto intro!: INF_eq) by (metis linorder_class.linear linorder_class.max.cobounded1 linorder_class.max.idem ord_class.atLeast_iff) lemma at_top_within_at_top_unbounded_rightI: fixes a::"'a::linorder" assumes "{a..} \ s" shows "at_top_within s = at_top" unfolding at_top_within_def at_top_def apply (auto intro!: INF_eq) apply (meson Ici_subset_Ioi_iff Ioi_le_Ico assms dual_order.refl dual_order.trans leI) by (metis assms atLeast_iff atLeast_subset_iff inf.cobounded1 linear subsetD) lemma at_top_within_at_top_bounded_right: fixes a b::"'a::{dense_order,linorder_topology}" assumes "a < b" shows "at_top_within {a.. {}" shows "eventually P (at_top_within s) \ (\x0::'a::{linorder_topology} \ s. \x \ x0. x\ s \ P x)" unfolding at_top_within_def apply (subst eventually_INF_base) apply (auto simp:eventually_principal sn) by (metis atLeast_subset_iff inf.coboundedI2 inf_commute linear) lemma tendsto_at_top_withinI: fixes f::"'a::linorder_topology \ 'b::metric_space" assumes "s \ {}" assumes "\e. 0 < e \ \x0 \ s. \x \ {x0..} \ s. dist (f x) l < e" shows "(f \ l) (at_top_within s)" apply(intro tendstoI) unfolding at_top_within_def apply (subst eventually_INF_base) apply (auto simp:eventually_principal assms) by (metis atLeast_subset_iff inf.coboundedI2 inf_commute linear) lemma tendsto_at_top_withinE: fixes f::"'a::linorder_topology \ 'b::metric_space" assumes "s \ {}" assumes "(f \ l) (at_top_within s)" assumes "e > 0" obtains x0 where "x0 \ s" "\x. x \ {x0..} \ s \ dist (f x) l < e" proof - from assms(2)[THEN tendstoD, OF assms(3)] have "\\<^sub>F x in at_top_within s. dist (f x) l < e" . then show ?thesis unfolding eventually_at_top_within_linorder[OF \s \ {}\] by (auto intro: that) qed lemma tendsto_at_top_within_iff: fixes f::"'a::linorder_topology \ 'b::metric_space" assumes "s \ {}" shows "(f \ l) (at_top_within s) \ (\e>0. \x0 \ s. \x \ {x0..} \ s. dist (f x) l < e)" by (auto intro!: tendsto_at_top_withinI[OF \s \ {}\] elim!: tendsto_at_top_withinE[OF \s \ {}\]) lemma filterlim_at_top_at_top_within_bounded_right: fixes a b::"'a::{dense_order,linorder_topology}" fixes f::"'a \ real" assumes "a < b" shows "filterlim f at_top (at_top_within {.. \) (at_left b)" unfolding filterlim_at_top_dense at_top_within_at_top_bounded_right'[OF assms(1)] eventually_at_left[OF assms(1)] tendsto_PInfty by auto text \Extract a sequence (going to infinity) bounded away from l\ lemma not_tendsto_frequentlyE: assumes "\((f \ l) F)" obtains S where "open S" "l \ S" "\\<^sub>F x in F. f x \ S" using assms by (auto simp: tendsto_def not_eventually) lemma not_tendsto_frequently_metricE: assumes "\((f \ l) F)" obtains e where "e > 0" "\\<^sub>F x in F. e \ dist (f x) l" using assms by (auto simp: tendsto_iff not_eventually not_less) lemma eventually_frequently_conj: "frequently P F \ eventually Q F \ frequently (\x. P x \ Q x) F" unfolding frequently_def apply (erule contrapos_nn) subgoal premises prems using prems by eventually_elim auto done lemma frequently_at_top: "(\\<^sub>F t in at_top. P t) \ (\t0. \t>t0. P t)" for P::"'a::{linorder,no_top}\bool" by (auto simp: frequently_def eventually_at_top_dense) lemma frequently_at_topE: fixes P::"nat \ 'a::{linorder,no_top}\_" assumes freq[rule_format]: "\n. \\<^sub>F a in at_top. P n a" obtains s::"nat\'a" where "\i. P i (s i)" "strict_mono s" proof - have "\f. \n. P n (f n) \ f n < f (Suc n)" proof (rule dependent_nat_choice) from frequently_ex[OF freq[of 0]] show "\x. P 0 x" . fix x n assume "P n x" from freq[unfolded frequently_at_top, rule_format, of x "Suc n"] obtain y where "P (Suc n) y" "y > x" by auto then show "\y. P (Suc n) y \ x < y" by auto qed then obtain s where "\i. P i (s i)" "strict_mono s" unfolding strict_mono_Suc_iff by auto then show ?thesis .. qed lemma frequently_at_topE': fixes P::"nat \ 'a::{linorder,no_top}\_" assumes freq[rule_format]: "\n. \\<^sub>F a in at_top. P n a" and g: "filterlim g at_top sequentially" obtains s::"nat\'a" where "\i. P i (s i)" "strict_mono s" "\n. g n \ s n" proof - have "\n. \\<^sub>F a in at_top. P n a \ g n \ a" using freq by (auto intro!: eventually_frequently_conj) from frequently_at_topE[OF this] obtain s where "\i. P i (s i)" "strict_mono s" "\n. g n \ s n" by metis then show ?thesis .. qed lemma frequently_at_top_at_topE: fixes P::"nat \ 'a::{linorder,no_top}\_" and g::"nat\'a" assumes "\n. \\<^sub>F a in at_top. P n a" "filterlim g at_top sequentially" obtains s::"nat\'a" where "\i. P i (s i)" "filterlim s at_top sequentially" proof - from frequently_at_topE'[OF assms] obtain s where s: "(\i. P i (s i))" "strict_mono s" "(\n. g n \ s n)" by blast have s_at_top: "filterlim s at_top sequentially" by (rule filterlim_at_top_mono) (use assms s in auto) with s(1) show ?thesis .. qed (* Extract a strict monotone and sequence converging to something other than l *) lemma not_tendsto_convergent_seq: fixes f::"real \ 'a::metric_space" assumes X: "compact (X::'a set)" assumes im: "\x. x \ 0 \ f x \ X" assumes nl: "\ ((f \ (l::'a)) at_top)" obtains s k where "k \ X" "k \ l" "(f \ s) \ k" "strict_mono s" "\n. s n \ n" proof - from not_tendsto_frequentlyE[OF nl] obtain S where "open S" "l \ S" "\\<^sub>F x in at_top. f x \ S" . have "\n. \\<^sub>F x in at_top. f x \ S \ real n \ x" apply (rule allI) apply (rule eventually_frequently_conj) apply fact by (rule eventually_ge_at_top) from frequently_at_topE[OF this] obtain s where "\i. f (s i) \ S" and s: "strict_mono s" and s_ge: "(\i. real i \ s i)" by metis then have "0 \ s i" for i using dual_order.trans of_nat_0_le_iff by blast then have "\n. (f \ s) n \ X" using im by auto from X[unfolded compact_def, THEN spec, THEN mp, OF this] obtain k r where k: "k \ X" and r: "strict_mono r" and kLim: "(f \ s \ r) \ k" by metis have "k \ X - S" by (rule Lim_in_closed_set[of "X - S", OF _ _ _ kLim]) (auto simp: im \0 \ s _\ \\i. f (s i) \ S\ intro!: \open S\ X intro: compact_imp_closed) note k moreover have "k \ l" using \k \ X - S\ \l \ S\ by auto moreover have "(f \ (s \ r)) \ k" using kLim by (simp add: o_assoc) moreover have "strict_mono (s \ r)" using s r by (rule strict_mono_o) moreover have "\n. (s \ r) n \ n" using s_ge r by (metis comp_apply dual_order.trans of_nat_le_iff seq_suble) ultimately show ?thesis .. qed lemma harmonic_bound: shows "1 / 2 ^(Suc n) < 1 / real (Suc n)" proof (induction n) case 0 then show ?case by auto next case (Suc n) then show ?case by (smt frac_less2 of_nat_0_less_iff of_nat_less_two_power zero_less_Suc) qed lemma INF_bounded_imp_convergent_seq: fixes f::"real \ real" assumes cont: "continuous_on {a..} f" assumes bound: "\t. t \ a \ f t > l" assumes inf: "(INF t\{a..}. f t) = l" obtains s where "(f \ s) \ l" "\i. s i \ {a..}" "filterlim s at_top sequentially" proof - have bound': "t \ {a..} \ f t \ l" for t using bound[of t] by auto have limpt: "l islimpt f ` {a..}" proof - have "Inf (f ` {a..}) islimpt f ` {a..}" by (rule Inf_islimpt) (auto simp: inf intro!: bdd_belowI2[where m=l] dest: bound) then show ?thesis by (simp add: inf) qed from limpt_closed_imp_exploding_subsequence[OF cont closed_atLeast bound' limpt] obtain s where s: "(f \ s) \ l" "\i. s i \ {a..}" "compact C \ C \ {a..} \ \\<^sub>F i in sequentially. s i \ C" for C by metis have "\\<^sub>F i in sequentially. s i \ n" for n using s(3)[of "{a..n}"] s(2) by (auto elim!: eventually_mono) then have "filterlim s at_top sequentially" unfolding filterlim_at_top by auto from s(1) s(2) this show ?thesis .. qed (* Generalizes to other combinations of strict_mono and filterlim *) lemma filterlim_at_top_strict_mono: fixes s :: "_ \ 'a::linorder" fixes r :: "nat \ _" assumes "strict_mono s" assumes "strict_mono r" assumes "filterlim s at_top F" shows "filterlim (s \ r) at_top F" apply (rule filterlim_at_top_mono[OF assms(3)]) by (simp add: assms(1) assms(2) seq_suble strict_mono_leD) lemma LIMSEQ_lb: assumes fl: "s \ (l::real)" assumes u: "l < u" shows "\n0. \n\n0. s n < u" proof - from fl have "\no>0. \n\no. dist (s n) l < u-l" unfolding LIMSEQ_iff_nz using u by simp thus ?thesis using dist_real_def by fastforce qed (* Used to sharpen a tendsto with additional information*) lemma filterlim_at_top_choose_lower: assumes "filterlim s at_top sequentially" assumes "(f \ s) \ l" obtains t where "filterlim t at_top sequentially" "(f \ t) \ l" "\n. t n \ (b::real)" proof - obtain k where k: "\n \ k. s n \ b" using assms(1) unfolding filterlim_at_top eventually_sequentially by blast define t where "t = (\n. s (n+k))" then have "\n. t n \ b" using k by simp have "filterlim t at_top sequentially" using assms(1) unfolding filterlim_at_top eventually_sequentially t_def by (metis (full_types) add.commute trans_le_add2) from LIMSEQ_ignore_initial_segment[OF assms(2), of "k"] have "(\n. (f \ s) (n + k)) \ l" . then have "(f \ t) \ l" unfolding t_def o_def by simp show ?thesis using \(f \ t) \ l\ \\n. b \ t n\ \filterlim t at_top sequentially\ that by blast qed lemma frequently_at_top_realE: fixes P::"nat \ real \ bool" assumes "\n. \\<^sub>F t in at_top. P n t" obtains s::"nat\real" where "\i. P i (s i)" "filterlim s at_top at_top" by (metis assms frequently_at_top_at_topE[OF _ filterlim_real_sequentially]) lemma approachable_sequenceE: fixes f::"real \ 'a::metric_space" assumes "\t e. 0 \ t \ 0 < e \ \tt\t. dist (f tt) p < e" obtains s where "filterlim s at_top sequentially" "(f \ s) \ p" proof - have "\n. \\<^sub>F i in at_top. dist (f i) p < 1/real (Suc n)" unfolding frequently_at_top apply (auto ) subgoal for n m using assms[of "max 0 (m+1)" "1/(Suc n)"] by force done from frequently_at_top_realE[OF this] obtain s where s: "\i. dist (f (s i)) p < 1 / real (Suc i)" "filterlim s at_top sequentially" by metis note this(2) moreover have "(f o s) \ p" proof (rule tendstoI) fix e::real assume "e > 0" have "\\<^sub>F i in sequentially. 1 / real (Suc i) < e" apply (rule order_tendstoD[OF _ \0 < e\]) apply (rule real_tendsto_divide_at_top) apply (rule tendsto_intros) by (rule filterlim_compose[OF filterlim_real_sequentially filterlim_Suc]) then show "\\<^sub>F x in sequentially. dist ((f \ s) x) p < e" by eventually_elim (use dual_order.strict_trans s \e > 0\ in auto) qed ultimately show ?thesis .. qed lemma mono_inc_bdd_above_has_limit_at_topI: fixes f::"real \ real" assumes "mono f" assumes "\x. f x \ u" shows "\l. (f \ l) at_top" proof - define l where "l = Sup (range (\n. f (real n)))" have t:"(\n. f (real n)) \ l" unfolding l_def apply (rule LIMSEQ_incseq_SUP) apply (meson assms(2) bdd_aboveI2) by (meson assms(1) mono_def of_nat_mono) from tendsto_at_topI_sequentially_real[OF assms(1) t] have "(f \ l) at_top" . thus ?thesis by blast qed lemma gen_mono_inc_bdd_above_has_limit_at_topI: fixes f::"real \ real" assumes "\x y. x \ b \ x \ y \ f x \ f y" assumes "\x. x \ b \ f x \ u" shows "\l. (f \ l) at_top" proof - define ff where "ff = (\x. if x \ b then f x else f b)" have m1:"mono ff" unfolding ff_def mono_def using assms(1) by simp have m2:"\x. ff x \ u" unfolding ff_def using assms(2) by simp from mono_inc_bdd_above_has_limit_at_topI[OF m1 m2] obtain l where "(ff \ l) at_top" by blast thus ?thesis by (meson \(ff \ l) at_top\ ff_def tendsto_at_top_eq_left) qed lemma gen_mono_dec_bdd_below_has_limit_at_topI: fixes f::"real \ real" assumes "\x y. x \ b \ x \ y \ f x \ f y" assumes "\x. x \ b \ f x \ u" shows "\l. (f \ l) at_top" proof - define ff where "ff = (\x. if x \ b then f x else f b)" have m1:"mono (-ff)" unfolding ff_def mono_def using assms(1) by simp have m2:"\x. (-ff) x \ -u" unfolding ff_def using assms(2) by simp from mono_inc_bdd_above_has_limit_at_topI[OF m1 m2] obtain l where "(-ff \ l) at_top" by blast then have "(ff \ -l) at_top" using tendsto_at_top_eq_left tendsto_minus_cancel_left by fastforce thus ?thesis by (meson \(ff \ -l) at_top\ ff_def tendsto_at_top_eq_left) qed lemma infdist_closed: shows "closed ({z. infdist z S \ e})" by (auto intro!:closed_Collect_le simp add:continuous_on_infdist) (* TODO: this is a copy of LIMSEQ_norm_0 where the sequence is bounded above in norm by a geometric series *) lemma LIMSEQ_norm_0_pow: assumes "k > 0" "b > 1" assumes "\n::nat. norm (s n) \ k / b^n" shows "s \ 0" proof (rule metric_LIMSEQ_I) fix e assume "e > (0::real)" then have "k / e > 0" using assms(1) by auto obtain N where N: "b^(N::nat) > k / e" using assms(2) - using Elementary_Topology.real_arch_pow by blast + using real_arch_pow by blast then have "norm (s n) < e" if "n \ N" for n proof - have "k / b^n \ k / b^N" by (smt assms(1) assms(2) frac_le leD power_less_imp_less_exp that zero_less_power) also have " ... < e" using N by (metis \0 < e\ assms(2) less_trans mult.commute pos_divide_less_eq zero_less_one zero_less_power) finally show ?thesis by (meson assms less_eq_real_def not_le order_trans) qed then show "\no. \n\no. dist (s n) 0 < e" by auto qed lemma filterlim_apply_filtermap: assumes g: "filterlim g G F" shows "filterlim (\x. m (g x)) (filtermap m G) F" by (metis filterlim_def filterlim_filtermap filtermap_mono g) lemma eventually_at_right_field_le: "eventually P (at_right x) \ (\b>x. \y>x. y \ b \ P y)" for x :: "'a::{linordered_field, linorder_topology}" by (smt dense eventually_at_right_field le_less_trans less_le_not_le order.strict_trans1) subsection \indexing euclidean space with natural numbers\ definition nth_eucl :: "'a::executable_euclidean_space \ nat \ real" where "nth_eucl x i = x \ (Basis_list ! i)" \ \TODO: why is that and some sort of \lambda_eucl\ nowhere available?\ definition lambda_eucl :: "(nat \ real) \ 'a::executable_euclidean_space" where "lambda_eucl (f::nat\real) = (\iR Basis_list ! i)" lemma eucl_eq_iff: "x = y \ (\ie i = xs ! i" if "length xs = DIM('a::executable_euclidean_space)" "i < DIM('a)" using that apply (auto simp: nth_eucl_def) by (metis list_of_eucl_eucl_of_list list_of_eucl_nth) lemma eucl_of_list_inner: "(eucl_of_list xs::'a) \ eucl_of_list ys = (\(x,y)\zip xs ys. x * y)" if "length xs = DIM('a::executable_euclidean_space)" "length ys = DIM('a::executable_euclidean_space)" using that by (auto simp: nth_eucl_def eucl_of_list_inner_eq inner_lv_rel_def) lemma self_eq_eucl_of_list: "x = eucl_of_list (map (\i. x $\<^sub>e i) [0..e i * y $\<^sub>e i)" for x y::"'a::executable_euclidean_space" apply (subst self_eq_eucl_of_list[where x=x]) apply (subst self_eq_eucl_of_list[where x=y]) apply (subst eucl_of_list_inner) by (auto simp: map2_map_map atLeast_upt interv_sum_list_conv_sum_set_nat) lemma norm_nth_eucl: "norm x = L2_set (\i. x $\<^sub>e i) {..e i = x $\<^sub>e i + y $\<^sub>e i" and minus_nth_eucl: "(x - y) $\<^sub>e i = x $\<^sub>e i - y $\<^sub>e i" and uminus_nth_eucl: "(-x) $\<^sub>e i = - x $\<^sub>e i" and scaleR_nth_eucl: "(c *\<^sub>R x) $\<^sub>e i = c *\<^sub>R (x $\<^sub>e i)" by (auto simp: nth_eucl_def algebra_simps) lemma inf_nth_eucl: "inf x y $\<^sub>e i = min (x $\<^sub>e i) (y $\<^sub>e i)" if "i < DIM('a)" for x::"'a::executable_euclidean_space" by (auto simp: nth_eucl_def algebra_simps inner_Basis_inf_left that inf_min) lemma sup_nth_eucl: "sup x y $\<^sub>e i = max (x $\<^sub>e i) (y $\<^sub>e i)" if "i < DIM('a)" for x::"'a::executable_euclidean_space" by (auto simp: nth_eucl_def algebra_simps inner_Basis_sup_left that sup_max) lemma le_iff_le_nth_eucl: "x \ y \ (\ie i) \ (y $\<^sub>e i))" for x::"'a::executable_euclidean_space" apply (auto simp: nth_eucl_def algebra_simps eucl_le[where 'a='a]) by (meson eucl_le eucl_le_Basis_list_iff) lemma eucl_less_iff_less_nth_eucl: "eucl_less x y \ (\ie i) < (y $\<^sub>e i))" for x::"'a::executable_euclidean_space" apply (auto simp: nth_eucl_def algebra_simps eucl_less_def[where 'a='a]) by (metis Basis_zero eucl_eq_iff inner_not_same_Basis inner_zero_left length_Basis_list nth_Basis_list_in_Basis nth_eucl_def) lemma continuous_on_nth_eucl[continuous_intros]: "continuous_on X (\x. f x $\<^sub>e i)" if "continuous_on X f" by (auto simp: nth_eucl_def intro!: continuous_intros that) subsection \derivatives\ lemma eventually_at_ne[intro, simp]: "\\<^sub>F x in at x0. x \ x0" by (auto simp: eventually_at_filter) lemma has_vector_derivative_withinD: fixes f::"real \ 'b::euclidean_space" assumes "(f has_vector_derivative f') (at x0 within S)" shows "((\x. (f x - f x0) /\<^sub>R (x - x0)) \ f') (at x0 within S)" apply (rule LIM_zero_cancel) apply (rule tendsto_norm_zero_cancel) apply (rule Lim_transform_eventually) proof - show "\\<^sub>F x in at x0 within S. norm ((f x - f x0 - (x - x0) *\<^sub>R f') /\<^sub>R norm (x - x0)) = norm ((f x - f x0) /\<^sub>R (x - x0) - f')" (is "\\<^sub>F x in _. ?th x") unfolding eventually_at_filter proof (safe intro!: eventuallyI) fix x assume x: "x \ x0" then have "norm ((f x - f x0) /\<^sub>R (x - x0) - f') = norm (sgn (x - x0) *\<^sub>R ((f x - f x0) /\<^sub>R (x - x0) - f'))" by simp also have "sgn (x - x0) *\<^sub>R ((f x - f x0) /\<^sub>R (x - x0) - f') = ((f x - f x0) /\<^sub>R norm (x - x0) - (x - x0) *\<^sub>R f' /\<^sub>R norm (x - x0))" by (auto simp add: algebra_simps sgn_div_norm divide_simps) (metis add.commute add_divide_distrib diff_add_cancel scaleR_add_left) also have "\ = (f x - f x0 - (x - x0) *\<^sub>R f') /\<^sub>R norm (x - x0)" by (simp add: algebra_simps) finally show "?th x" .. qed show "((\x. norm ((f x - f x0 - (x - x0) *\<^sub>R f') /\<^sub>R norm (x - x0))) \ 0) (at x0 within S)" by (rule tendsto_norm_zero) (use assms in \auto simp: has_vector_derivative_def has_derivative_at_within\) qed text \A \path_connected\ set \S\ entering both \T\ and \-T\ must cross the frontier of \T\ \ lemma path_connected_frontier: fixes S :: "'a::real_normed_vector set" assumes "path_connected S" assumes "S \ T \ {}" assumes "S \ -T \ {}" obtains s where "s \ S" "s \ frontier T" proof - obtain st where st:"st \ S \ T" using assms(2) by blast obtain sn where sn:"sn \ S \ -T" using assms(3) by blast obtain g where g: "path g" "path_image g \ S" "pathstart g = st" "pathfinish g = sn" using assms(1) st sn unfolding path_connected_def by blast have a1:"pathstart g \ closure T" using st g(3) closure_Un_frontier by fastforce have a2:"pathfinish g \ T" using sn g(4) by auto from exists_path_subpath_to_frontier[OF g(1) a1 a2] obtain h where "path_image h \ path_image g" "pathfinish h \ frontier T" by metis thus ?thesis using g(2) by (meson in_mono pathfinish_in_path_image that) qed lemma path_connected_not_frontier_subset: fixes S :: "'a::real_normed_vector set" assumes "path_connected S" assumes "S \ T \ {}" assumes "S \ frontier T = {}" shows "S \ T" using path_connected_frontier assms by auto lemma compact_attains_bounds: fixes f::"'a::topological_space \ 'b::linorder_topology" assumes compact: "compact S" assumes ne: "S \ {}" assumes cont: "continuous_on S f" obtains l u where "l \ S" "u \ S" "\x. x \ S \ f x \ {f l .. f u}" proof - from compact_continuous_image[OF cont compact] have compact_image: "compact (f ` S)" . have ne_image: "f ` S \ {}" using ne by simp from compact_attains_inf[OF compact_image ne_image] obtain l where "l \ S" "\x. x \ S \ f l \ f x" by auto moreover from compact_attains_sup[OF compact_image ne_image] obtain u where "u \ S" "\x. x \ S \ f x \ f u" by auto ultimately have "l \ S" "u \ S" "\x. x \ S \ f x \ {f l .. f u}" by auto then show ?thesis .. qed lemma uniform_limit_const[uniform_limit_intros]: "uniform_limit S (\x y. f x) (\_. l) F" if "(f \ l) F" apply (auto simp: uniform_limit_iff) subgoal for e using tendstoD[OF that(1), of e] by (auto simp: eventually_mono) done subsection \Segments\ text \\closed_segment\ throws away the order that our intuition keeps\ definition line::"'a::real_vector \ 'a \ real \ 'a" ("{_ -- _}\<^bsub>_\<^esub>") where "{a -- b}\<^bsub>u\<^esub> = a + u *\<^sub>R (b - a)" abbreviation "line_image a b U \(\u. {a -- b}\<^bsub>u\<^esub>) ` U" notation line_image ("{_ -- _}\<^bsub>`_\<^esub>") lemma in_closed_segment_iff_line: "x \ {a -- b} \ (\c\{0..1}. x = line a b c)" by (auto simp: in_segment line_def algebra_simps) lemma in_open_segment_iff_line: "x \ {a <--< b} \ (\c\{0<..<1}. a \ b \ x = line a b c)" by (auto simp: in_segment line_def algebra_simps) lemma line_convex_combination1: "(1 - u) *\<^sub>R line a b i + u *\<^sub>R b = line a b (i + u - i * u)" by (auto simp: line_def algebra_simps) lemma line_convex_combination2: "(1 - u) *\<^sub>R a + u *\<^sub>R line a b i = line a b (i*u)" by (auto simp: line_def algebra_simps) lemma line_convex_combination12: "(1 - u) *\<^sub>R line a b i + u *\<^sub>R line a b j = line a b (i + u * (j - i))" by (auto simp: line_def algebra_simps) lemma mult_less_one_less_self: "0 < x \ i < 1 \ i * x < x" for i x::real by auto lemma plus_times_le_one_lemma: "i + u - i * u \ 1" if "i \ 1" "u \ 1" for i u::real by (simp add: diff_le_eq sum_le_prod1 that) lemma plus_times_less_one_lemma: "i + u - i * u < 1" if "i < 1" "u < 1" for i u::real proof - have "u * (1 - i) < 1 - i" using that by force then show ?thesis by (simp add: algebra_simps) qed lemma line_eq_endpoint_iff[simp]: "line a b i = b \ (a = b \ i = 1)" "a = line a b i \ (a = b \ i = 0)" by (auto simp: line_def algebra_simps) lemma line_eq_iff[simp]: "line a b x = line a b y \ (x = y \ a = b)" by (auto simp: line_def) lemma line_open_segment_iff: "{line a b i<-- b" using that apply (auto simp: in_segment line_convex_combination1 plus_times_less_one_lemma) subgoal for j apply (rule exI[where x="(j - i)/(1 - i)"]) apply (auto simp: divide_simps algebra_simps) by (metis add_diff_cancel less_numeral_extra(4) mult_2_right plus_times_less_one_lemma that(1)) done lemma open_segment_line_iff: "{a<-- b" using that apply (auto simp: in_segment line_convex_combination2 plus_times_less_one_lemma) subgoal for j apply (rule exI[where x="j/i"]) by (auto simp: ) done lemma line_closed_segment_iff: "{line a b i--b} = line a b ` {i..1}" if "i \ 1" "a \ b" using that apply (auto simp: in_segment line_convex_combination1 mult_le_cancel_right2 plus_times_le_one_lemma) subgoal for j apply (rule exI[where x="(j - i)/(1 - i)"]) apply (auto simp: divide_simps algebra_simps) by (metis add_diff_cancel less_numeral_extra(4) mult_2_right plus_times_less_one_lemma that(1)) done lemma closed_segment_line_iff: "{a--line a b i} = line a b ` {0..i}" if "0 < i" "a \ b" using that apply (auto simp: in_segment line_convex_combination2 plus_times_less_one_lemma) subgoal for j apply (rule exI[where x="j/i"]) by (auto simp: ) done lemma closed_segment_line_line_iff: "{line a b i1--line a b i2} = line a b ` {i1..i2}" if "i1 \ i2" using that apply (auto simp: in_segment line_convex_combination12 intro!: imageI) apply (smt mult_left_le_one_le) subgoal for u by (rule exI[where x="(u - i1)/(i2-i1)"]) auto done lemma line_line1: "line (line a b c) b x = line a b (c + x - c * x)" by (simp add: line_def algebra_simps) lemma line_line2: "line a (line a b c) x = line a b (c*x)" by (simp add: line_def algebra_simps) lemma line_in_subsegment: "i1 < 1 \ i2 < 1 \ a \ b \ line a b i1 \ {line a b i2<-- i2 < i1" by (auto simp: line_open_segment_iff intro!: imageI) lemma line_in_subsegment2: "0 < i2 \ 0 < i1 \ a \ b \ line a b i1 \ {a<-- i1 < i2" by (auto simp: open_segment_line_iff intro!: imageI) lemma line_in_open_segment_iff[simp]: "line a b i \ {a<-- (a \ b \ 0 < i \ i < 1)" by (auto simp: in_open_segment_iff_line) subsection \Open Segments\ lemma open_segment_subsegment: assumes "x1 \ {x0<-- {x1<-- {x0<-- \TODO: use \line\\ from assms obtain u v::real where ne: "x0 \ x3" "(1 - u) *\<^sub>R x0 + u *\<^sub>R x3 \ x3" and x1_def: "x1 = (1 - u) *\<^sub>R x0 + u *\<^sub>R x3" and x2_def: "x2 = (1 - v) *\<^sub>R ((1 - u) *\<^sub>R x0 + u *\<^sub>R x3) + v *\<^sub>R x3" and uv: \0 < u\ \0 < v\ \u < 1\ \v < 1\ by (auto simp: in_segment) let ?d = "(u + v - u * v)" have "?d > 0" using uv by (auto simp: add_nonneg_pos pos_add_strict) with \x0 \ x3\ have "0 \ ?d *\<^sub>R (x3 - x0)" by simp moreover define ua where "ua = u / ?d" have "ua * (u * v - u - v) - - u = 0" by (auto simp: ua_def algebra_simps divide_simps) (metis uv add_less_same_cancel1 add_strict_mono mult.right_neutral mult_less_cancel_left_pos not_real_square_gt_zero vector_space_over_itself.scale_zero_left) then have "(ua * (u * v - u - v) - - u) *\<^sub>R (x3 - x0) = 0" by simp moreover have "0 < ua" "ua < 1" using \0 < u\ \0 < v\ \u < 1\ \v < 1\ by (auto simp: ua_def pos_add_strict intro!: divide_pos_pos) ultimately show ?thesis unfolding x1_def x2_def by (auto intro!: exI[where x=ua] simp: algebra_simps in_segment) qed subsection \Syntax\ abbreviation sequentially_at_top::"(nat\real)\bool" ("_ \\<^bsub>\<^esub> \") \ \the \\<^bsub>\<^esub>\ is to disambiguate syntax...\ where "s \\<^bsub>\<^esub> \ \ filterlim s at_top sequentially" abbreviation sequentially_at_bot::"(nat\real)\bool" ("_ \\<^bsub>\<^esub> -\") where "s \\<^bsub>\<^esub> -\ \ filterlim s at_bot sequentially" subsection \Paths\ lemma subpath0_linepath: shows "subpath 0 u (linepath t t') = linepath t (t + u * (t' - t))" unfolding subpath_def linepath_def apply (rule ext) apply auto proof - fix x :: real have f1: "\r ra rb rc. (r::real) + ra * rb - ra * rc = r - ra * (rc - rb)" by (simp add: right_diff_distrib') have f2: "\r ra. (r::real) - r * ra = r * (1 - ra)" by (simp add: right_diff_distrib') have f3: "\r ra rb. (r::real) - ra + rb + ra - r = rb" by auto have f4: "\r. (r::real) + (1 - 1) = r" by linarith have f5: "\r ra. (r::real) + ra = ra + r" by force have f6: "\r ra. (r::real) + (1 - (r + 1) + ra) = ra" by linarith have "t - x * (t - (t + u * (t' - t))) = t' * (u * x) + (t - t * (u * x))" by (simp add: right_diff_distrib') then show "(1 - u * x) * t + u * x * t' = (1 - x) * t + x * (t + u * (t' - t))" using f6 f5 f4 f3 f2 f1 by (metis (no_types) mult.commute) qed lemma linepath_image0_right_open_real: assumes "t < (t'::real)" shows "linepath t t' ` {0..<1} = {t.. x" "x < t'" let ?u = "(x-t)/(t'-t)" have "?u \ 0" using \t \ x\ assms by auto moreover have "?u < 1" by (simp add: \x < t'\ assms) moreover have "x = (1-?u) * t + ?u*t'" proof - have f1: "\r ra. (ra::real) * - r = r * - ra" by simp have "t + (t' + - t) * ((x + - t) / (t' + - t)) = x" using assms by force then have "t' * ((x + - t) / (t' + - t)) + t * (1 + - ((x + - t) / (t' + - t))) = x" using f1 by (metis (no_types) add.left_commute distrib_left mult.commute mult.right_neutral) then show ?thesis by (simp add: mult.commute) qed ultimately show "x \ (\x. (1 - x) * t + x * t') ` {0..<1}" using atLeastLessThan_iff by blast qed lemma oriented_subsegment_scale: assumes "x1 \ {a<-- {x1<-- 0" "b-a = e *\<^sub>R (x2-x1)" proof - from assms(1) obtain u where u : "u > 0" "u < 1" "x1 = (1 - u) *\<^sub>R a + u *\<^sub>R b" unfolding in_segment by blast from assms(2) obtain v where v: "v > 0" "v < 1" "x2 = (1 - v) *\<^sub>R x1 + v *\<^sub>R b" unfolding in_segment by blast have "x2-x1 = -v *\<^sub>R x1 + v *\<^sub>R b" using v by (metis add.commute add_diff_cancel_right diff_minus_eq_add scaleR_collapse scaleR_left.minus) also have "... = (-v) *\<^sub>R ((1 - u) *\<^sub>R a + u *\<^sub>R b) + v *\<^sub>R b" using u by auto also have "... = v *\<^sub>R ((1-u)*\<^sub>R b - (1-u)*\<^sub>R a )" by (smt add_diff_cancel diff_diff_add diff_minus_eq_add minus_diff_eq scaleR_collapse scale_minus_left scale_right_diff_distrib) finally have x2x1:"x2-x1 = (v *(1-u)) *\<^sub>R (b - a)" by (metis scaleR_scaleR scale_right_diff_distrib) have "v * (1-u) > 0" using u(2) v(1) by simp then have "(x2-x1)/\<^sub>R (v * (1-u)) = (b-a)" unfolding x2x1 by (smt field_class.field_inverse scaleR_one scaleR_scaleR) thus ?thesis using \0 < v * (1 - u)\ positive_imp_inverse_positive that by fastforce qed end diff --git a/thys/Poincare_Bendixson/Limit_Set.thy b/thys/Poincare_Bendixson/Limit_Set.thy --- a/thys/Poincare_Bendixson/Limit_Set.thy +++ b/thys/Poincare_Bendixson/Limit_Set.thy @@ -1,473 +1,473 @@ section \Limit Sets\ theory Limit_Set imports Invariance begin context auto_ll_on_open begin text \Positive limit point, assuming \{0..} \ existence_ivl0 x\\ (* TODO: Perhaps a more intrinsic definition would be better here *) definition "\_limit_point x p \ {0..} \ existence_ivl0 x \ (\s. s \\<^bsub>\<^esub> \ \ (flow0 x \ s) \ p)" text \ Also called the \\\-limit set of x \ definition "\_limit_set x = {p. \_limit_point x p}" definition "\_limit_point x p \ {..0} \ existence_ivl0 x \ (\s. s \\<^bsub>\<^esub> -\ \ (flow0 x \ s) \ p)" text \ Also called the \\\-limit set of x \ definition "\_limit_set x = {p. \_limit_point x p}" end context auto_ll_on_open begin lemma \_limit_point_eq_rev: "\_limit_point x p = rev.\_limit_point x p" unfolding \_limit_point_def rev.\_limit_point_def apply (auto simp: rev_eq_flow[abs_def] o_def filterlim_uminus_at_bot rev_existence_ivl_eq0 subset_iff intro: exI[where x="uminus o s" for s]) using neg_0_le_iff_le by fastforce lemma \_limit_set_eq_rev: "\_limit_set x = rev.\_limit_set x" unfolding \_limit_set_def rev.\_limit_set_def \_limit_point_eq_rev .. lemma \_limit_pointE: assumes "\_limit_point x p" obtains s where "filterlim s at_top sequentially" "(flow0 x \ s) \ p" "\n. b \ s n" using assms filterlim_at_top_choose_lower \_limit_point_def by blast lemma \_limit_set_eq: assumes "{0..} \ existence_ivl0 x" shows "\_limit_set x = (INF \ \ {0..}. closure (flow0 x ` {\..}))" unfolding \_limit_set_def proof safe fix p t assume pt: "0 \ (t::real)" "\_limit_point x p" from \_limit_pointE[OF pt(2)] obtain s where "filterlim s at_top sequentially" "(flow0 x \ s) \ p" "\n. t \ s n" by blast thus "p \ closure (flow0 x ` {t..})" unfolding closure_sequential by (metis atLeast_iff comp_apply imageI) next fix p assume "p \ (\\\{0..}. closure (flow0 x ` {\..}))" then have "\t. t \0 \ p \ closure (flow0 x ` {t..})" by blast then have "\t e. t \0 \ e > 0 \ (\tt \ t. dist (flow0 x tt) p < e)" unfolding closure_approachable by fastforce from approachable_sequenceE[OF this] obtain s where "filterlim s at_top sequentially" "(flow0 x \ s) \ p" by auto thus "\_limit_point x p" unfolding \_limit_point_def using assms by auto qed lemma \_limit_set_empty: assumes "\ ({0..} \ existence_ivl0 x)" shows "\_limit_set x = {}" unfolding \_limit_set_def \_limit_point_def by (simp add: assms) lemma \_limit_set_closed: "closed (\_limit_set x)" using \_limit_set_eq by (metis \_limit_set_empty closed_INT closed_closure closed_empty) (* TODO: Walter gives a more direct proof *) lemma \_limit_set_positively_invariant: shows "positively_invariant (\_limit_set x)" unfolding positively_invariant_def trapped_forward_def proof safe fix dummy p t assume xa: "p \ \_limit_set x" "t \ existence_ivl0 p" "0 \ t" have "p \ X" using mem_existence_ivl_iv_defined(2) xa(2) by blast have exist: "{0..} \ existence_ivl0 x" using xa(1) unfolding \_limit_set_def \_limit_point_def by auto from xa(1) obtain s where s: "filterlim s at_top sequentially" "(flow0 x \ s) \ p" "\n. 0 \ s n" unfolding \_limit_set_def by (auto elim!:\_limit_pointE) define r where "r = (\n. t + s n)" have rlim: "filterlim r at_top sequentially" unfolding r_def by (auto intro: filterlim_tendsto_add_at_top[OF _ s(1)]) define dom where "dom = image (flow0 x) {0..} \ {p} " have domin: "\n. (flow0 x \ s) n \ dom" "p \ dom" unfolding dom_def o_def using exist by(auto simp add: s(3)) have xt: "\x. x \ dom \ t \ existence_ivl0 x" unfolding dom_def using xa(2) apply auto apply (rule existence_ivl_trans') using exist xa(3) apply auto[1] using exist by auto have cont: "continuous_on dom (\x. flow0 x t)" apply (rule flow_continuous_on_compose) apply auto using \p \ X\ exist local.dom_def local.flow_in_domain apply auto[1] using xt . then have f1: "((\x. flow0 x t) \ (flow0 x \ s)) \ flow0 p t" using domin s(2) unfolding continuous_on_sequentially by blast have ff:"\n. (flow0 x \ r) n = ((\x. flow0 x t) \ (flow0 x \ s)) n" unfolding o_def r_def proof - fix n have s:"s n \ existence_ivl0 x" using s(3) exist by auto then have t:"t \ existence_ivl0 (flow0 x (s n))" using domin(1) xt by auto from flow_trans[OF s t] show "flow0 x (t + s n) = flow0 (flow0 x (s n)) t" by (simp add: add.commute) qed have f2: "(flow0 x \ r) \ flow0 p t" using f1 unfolding ff . show "flow0 p t \ \_limit_set x" using exist f2 rlim unfolding \_limit_set_def \_limit_point_def using flow_in_domain r_def s(3) xa(2) xa(3) by auto qed lemma \_limit_set_invariant: shows "invariant (\_limit_set x)" unfolding invariant_iff_pos_invariant_and_compl_pos_invariant proof safe show "positively_invariant (\_limit_set x)" using \_limit_set_positively_invariant . next show "positively_invariant (X - \_limit_set x)" unfolding positively_invariant_def trapped_forward_def apply safe using local.flow_in_domain apply blast proof - fix dummy p t assume xa: "p \ X" "p \ \_limit_set x" "t \ existence_ivl0 p" "0 \ t" and f: "flow0 p t \ \_limit_set x" have exist: "{0..} \ existence_ivl0 x" using f unfolding \_limit_set_def \_limit_point_def by auto from f obtain s where s: "filterlim s at_top sequentially" "(flow0 x \ s) \ flow0 p t" "\n. t \ s n" unfolding \_limit_set_def by (auto elim!:\_limit_pointE) define r where "r = (\n. (-t) + s n)" have "(\x. -t) \ -t" by simp from filterlim_tendsto_add_at_top[OF this s(1)] have rlim: "filterlim r at_top sequentially" unfolding r_def by simp define dom where "dom = image (flow0 x) {t..} \ {flow0 p t} " have domin: "\n. (flow0 x \ s) n \ dom" "flow0 p t \ dom" unfolding dom_def o_def using exist by(auto simp add: s(3)) have xt: "\x. x \ dom \ -t \ existence_ivl0 x" unfolding dom_def using xa(2) apply auto using local.existence_ivl_reverse xa(3) apply auto[1] by (metis exist atLeast_iff diff_conv_add_uminus diff_ge_0_iff_ge linordered_ab_group_add_class.zero_le_double_add_iff_zero_le_single_add local.existence_ivl_trans' order_trans subset_iff xa(4)) have cont: "continuous_on dom (\x. flow0 x (-t))" apply (rule flow_continuous_on_compose) apply auto using local.mem_existence_ivl_iv_defined(2) xt apply blast by (simp add: xt) then have f1: "((\x. flow0 x (-t)) \ (flow0 x \ s)) \ flow0 (flow0 p t) (-t)" using domin s(2) unfolding continuous_on_sequentially by blast have ff:"\n. (flow0 x \ r) n = ((\x. flow0 x (-t)) \ (flow0 x \ s)) n" unfolding o_def r_def proof - fix n have s:"s n \ existence_ivl0 x" using s(3) exist \0\ t\ by (meson atLeast_iff order_trans subset_eq) then have t:"-t \ existence_ivl0 (flow0 x (s n))" using domin(1) xt by auto from flow_trans[OF s t] show "flow0 x (-t + s n) = flow0 (flow0 x (s n)) (-t)" by (simp add: add.commute) qed have "(flow0 x \ r) \ flow0 (flow0 p t) (-t)" using f1 unfolding ff . then have f2: "(flow0 x \ r) \ p" using flows_reverse xa(3) by auto then have "p \ \_limit_set x" unfolding \_limit_set_def \_limit_point_def using rlim exist by auto thus False using xa(2) by auto qed qed end context auto_ll_on_open begin lemma \_limit_set_eq: assumes "{..0} \ existence_ivl0 x" shows "\_limit_set x = (INF \ \ {..0}. closure (flow0 x ` {..\}))" using rev.\_limit_set_eq[of x, OF assms[folded infinite_rev_existence_ivl0_rewrites]] unfolding \_limit_set_eq_rev rev_flow_image_eq image_uminus_atLeast by (smt INT_extend_simps(10) Sup.SUP_cong image_uminus_atMost) lemma \_limit_set_closed: shows "closed (\_limit_set x)" unfolding \_limit_set_eq_rev by (rule rev.\_limit_set_closed) lemma \_limit_set_positively_invariant: shows "negatively_invariant (\_limit_set x)" unfolding negatively_invariant_eq_rev \_limit_set_eq_rev by (simp add: rev.\_limit_set_positively_invariant) lemma \_limit_set_invariant: shows "invariant (\_limit_set x)" unfolding invariant_eq_rev \_limit_set_eq_rev by (simp add: rev.\_limit_set_invariant) text \ Fundamental properties of the positive limit set \ context fixes x K assumes K: "compact K" "K \ X" assumes x: "x \ X" "trapped_forward x K" begin text \Bunch of facts for what's to come\ private lemma props: shows "{0..} \ existence_ivl0 x" "seq_compact K" apply (rule trapped_sol_right) using x K by (auto simp add: compact_imp_seq_compact) private lemma flowimg: shows "flow0 x ` (existence_ivl0 x \ {0..}) = flow0 x ` {0..}" using props(1) by auto lemma \_limit_set_in_compact_subset: shows "\_limit_set x \ K" unfolding \_limit_set_def proof safe fix p s assume "\_limit_point x p" from \_limit_pointE[OF this] obtain s where s: "filterlim s at_top sequentially" "(flow0 x \ s) \ p" "\n. 0 \ s n" by blast then have fin: "\n. (flow0 x \ s) n \ K" using s(3) x K props(1) unfolding trapped_forward_def by (simp add: subset_eq) from seq_compactE[OF props(2) fin] show "p \ K" using s(2) by (metis LIMSEQ_subseq_LIMSEQ LIMSEQ_unique) qed lemma \_limit_set_in_compact_compact: shows "compact (\_limit_set x)" proof - from \_limit_set_in_compact_subset have "bounded (\_limit_set x)" using bounded_subset compact_imp_bounded using K(1) by auto thus ?thesis using \_limit_set_closed by (simp add: compact_eq_bounded_closed) qed lemma \_limit_set_in_compact_nonempty: shows "\_limit_set x \ {}" proof - have fin: "\n. (flow0 x \ real) n \ K" using x K props(1) by (simp add: flowimg image_subset_iff trapped_forward_def) from seq_compactE[OF props(2) this] obtain r l where "l \ K" "strict_mono r" "(flow0 x \ real \ r) \ l" by blast then have "\_limit_point x l" unfolding \_limit_point_def using props(1) by (smt comp_def filterlim_sequentially_iff_filterlim_real filterlim_subseq tendsto_at_top_eq_left) thus ?thesis unfolding \_limit_set_def by auto qed lemma \_limit_set_in_compact_existence: shows "\y. y \ \_limit_set x \ existence_ivl0 y = UNIV" proof - fix y assume y: "y \ \_limit_set x" then have "y \ X" using \_limit_set_in_compact_subset K by blast from \_limit_set_invariant have "\t. t \ existence_ivl0 y \ flow0 y t \ \_limit_set x" unfolding invariant_def trapped_iff_on_existence_ivl0 using y by blast then have t: "\t. t \ existence_ivl0 y \ flow0 y t \ K" using \_limit_set_in_compact_subset by blast thus "existence_ivl0 y = UNIV" by (meson \y \ X\ existence_ivl_zero existence_ivl_initial_time_iff existence_ivl_subset mem_compact_implies_subset_existence_interval subset_antisym K) qed lemma \_limit_set_in_compact_tendsto: shows "((\t. infdist (flow0 x t) (\_limit_set x)) \ 0) at_top" proof (rule ccontr) assume "\ ((\t. infdist (flow0 x t) (\_limit_set x)) \ 0) at_top" from not_tendsto_frequentlyE[OF this] obtain S where S: "open S" "0 \ S" "\\<^sub>F t in at_top. infdist (flow0 x t) (\_limit_set x) \ S" . then obtain e where "e > 0" "ball 0 e \ S" using openE by blast then have "\x. x \0 \ x \ S \ x \ e" by force then have "\xa. infdist (flow0 x xa) (\_limit_set x) \ S \ infdist (flow0 x xa) (\_limit_set x) \ e" using infdist_nonneg by blast from frequently_mono[OF this S(3)] have "\\<^sub>F t in at_top. infdist (flow0 x t) (\_limit_set x) \ e" by blast then have "\n. \\<^sub>F t in at_top. infdist (flow0 x t) (\_limit_set x) \ e \ real n \ t" by (auto intro!: eventually_frequently_conj) from frequently_at_topE[OF this] obtain s where s: "\i. e \ infdist (flow0 x (s i)) (\_limit_set x)" "\i. real i \ s i" "strict_mono s" by force then have sf: "filterlim s at_top sequentially" using filterlim_at_top_mono filterlim_real_sequentially not_eventuallyD by blast have fin: "\n. (flow0 x \ s) n \ K" using x K props(1) s unfolding flowimg trapped_forward_def by (metis atLeast_iff comp_apply image_subset_iff of_nat_0_le_iff order_trans) from seq_compactE[OF props(2) this] obtain r l where r:"strict_mono r" and l: "l \ K" "(flow0 x \ s \ r) \ l" by blast moreover from filterlim_at_top_strict_mono[OF s(3) r(1) sf] have "filterlim (s \ r) at_top sequentially" . moreover have "\_limit_point x l" unfolding \_limit_point_def using props(1) calculation by (metis comp_assoc) ultimately have "infdist l (\_limit_set x) = 0" by (simp add: \_limit_set_def) then have c1:"((\y. infdist y (\_limit_set x)) \ (flow0 x \ s \ r)) \ 0" - using l(2) continuous_on_infdist - by (metis UNIV_I continuous_on_sequentially) + by (auto intro!: tendsto_compose_at[OF l(2)] tendsto_eq_intros) have c2: "\i. e \ infdist (flow0 x ((s \ r) i)) (\_limit_set x)" using s(1) by simp show False using c1 c2 \e > 0\ unfolding o_def - using Lim_bounded2 s(1) by fastforce + using Lim_bounded2 + by (metis (no_types, lifting) ball_eq_empty centre_in_ball empty_iff) qed lemma \_limit_set_in_compact_connected: shows "connected (\_limit_set x)" unfolding connected_closed_set[OF \_limit_set_closed] proof clarsimp fix Apre Bpre assume pre: "closed Apre" "Apre \ Bpre = \_limit_set x" "closed Bpre" "Apre \ {}" "Bpre \ {}" "Apre \ Bpre = {}" (* TODO: this move is very strange *) then obtain A B where "Apre \ A" "Bpre \ B" "open A" "open B" and disj:"A \ B = {}" by (meson t4_space) then have "\_limit_set x \ A \ B" "\_limit_set x \ A \ {}" "\_limit_set x \ B \ {}" using pre by auto then obtain p q where p: "\_limit_point x p" "p \ A" and q: "\_limit_point x q" "q \ B" using \_limit_set_def by auto from \_limit_pointE[OF p(1)] obtain ps where ps: "filterlim ps at_top sequentially" "(flow0 x \ ps) \ p" "\n. 0 \ ps n" by blast from \_limit_pointE[OF q(1)] obtain qs where qs: "filterlim qs at_top sequentially" "(flow0 x \ qs) \ q" "\n. 0 \ qs n" by blast have "\n. \\<^sub>F t in at_top. flow0 x t \ A \ flow0 x t \ B" unfolding frequently_at_top proof safe fix dummy mpre obtain m where "m \ (0::real)" "m > mpre" by (meson approximation_preproc_push_neg(1) gt_ex le_cases order_trans) from ps obtain a where a:"a > m" "(flow0 x a) \ A" - using \open A\ p unfolding tendsto_explicit filterlim_at_top eventually_sequentially + using \open A\ p unfolding tendsto_def filterlim_at_top eventually_sequentially by (metis approximation_preproc_push_neg(1) comp_apply gt_ex le_cases order_trans) from qs obtain b where b:"b > a" "(flow0 x b) \ B" - using \open B\ q unfolding tendsto_explicit filterlim_at_top eventually_sequentially + using \open B\ q unfolding tendsto_def filterlim_at_top eventually_sequentially by (metis approximation_preproc_push_neg(1) comp_apply gt_ex le_cases order_trans) have "continuous_on {a..b} (flow0 x)" by (metis Icc_subset_Ici_iff \0 \ m\ \m < a\ approximation_preproc_push_neg(2) atMost_iff atMost_subset_iff continuous_on_subset le_cases local.flow_continuous_on props(1) subset_eq) from connected_continuous_image[OF this connected_Icc] have c:"connected (flow0 x ` {a..b})" . have "\t\ {a..b}. flow0 x t \ A \ flow0 x t \ B" proof (rule ccontr) assume "\ (\t\{a..b}. flow0 x t \ A \ flow0 x t \ B)" then have "flow0 x ` {a..b} \ A \ B" by blast - from connectedD[OF c \open A\ \open B\ this] + from topological_space_class.connectedD[OF c \open A\ \open B\ _ this] show False using a b disj by force qed thus "\n>mpre. flow0 x n \ A \ flow0 x n \ B" - by (smt \mpre < m\ a(1) atLeastAtMost_iff) + by (smt \mpre < m\ a(1) atLeastAtMost_iff) qed from frequently_at_topE'[OF this filterlim_real_sequentially] obtain s where s: "\i. flow0 x (s i) \ A \ flow0 x (s i) \ B" "strict_mono s" "\n. real n \ s n" by blast then have "\n. (flow0 x \ s) n \ K" by (smt atLeast_iff comp_apply flowimg image_subset_iff of_nat_0_le_iff trapped_forward_def x(2)) from seq_compactE[OF props(2) this] obtain r l where r: "l \ K" "strict_mono r" "(flow0 x \ s \ r) \ l" by blast have "filterlim s at_top sequentially" using s filterlim_at_top_mono filterlim_real_sequentially not_eventuallyD by blast from filterlim_at_top_strict_mono[OF s(2) r(2) this] have "filterlim (s \ r) at_top sequentially" . then have "\_limit_point x l" unfolding \_limit_point_def using props(1) r by (metis comp_assoc) - moreover have "l \ A" using s(1) r(3) \open A\ unfolding tendsto_explicit by auto - moreover have "l \ B" using s(1) r(3) \open B\ unfolding tendsto_explicit by auto + moreover have "l \ A" using s(1) r(3) \open A\ unfolding tendsto_def by auto + moreover have "l \ B" using s(1) r(3) \open B\ unfolding tendsto_def by auto ultimately show False using \\_limit_set x \ A \ B\ unfolding \_limit_set_def by auto qed lemma \_limit_set_in_compact_\_limit_set_contained: shows "\y \ \_limit_set x. \_limit_set y \ \_limit_set x" proof safe fix y z assume "y \ \_limit_set x" "z \ \_limit_set y" then have "\_limit_point y z" unfolding \_limit_set_def by auto from \_limit_pointE[OF this] obtain s where s: "(flow0 y \ s) \ z" . have "\n. (flow0 y \ s) n \ \_limit_set x" using \y \ \_limit_set x\ invariant_def \_limit_set_in_compact_existence \_limit_set_invariant trapped_iff_on_existence_ivl0 by force thus "z \ \_limit_set x" using closed_sequential_limits s \_limit_set_closed by blast qed lemma \_limit_set_in_compact_\_limit_set_contained: assumes zpx: "z \ \_limit_set x" shows "\_limit_set z \ \_limit_set x" proof fix w assume "w \ \_limit_set z" then obtain s where s: "(flow0 z \ s) \ w" unfolding \_limit_set_def \_limit_point_def by auto from \_limit_set_invariant have "invariant (\_limit_set x)" . then have "\n. (flow0 z \ s) n \ \_limit_set x" using \_limit_set_in_compact_existence[OF zpx] zpx using invariant_def trapped_iff_on_existence_ivl0 by fastforce from closed_sequentially[OF \_limit_set_closed this s] show "w \ \_limit_set x" . qed end text \ Fundamental properties of the negative limit set \ end context auto_ll_on_open begin context fixes x K assumes x: "x \ X" "trapped_backward x K" assumes K: "compact K" "K \ X" begin private lemma xrev: "x \ X" "rev.trapped_forward x K" using trapped_backward_iff_rev_trapped_forward x(2) by (auto simp: rev_existence_ivl_eq0 rev_eq_flow x(1)) lemma \_limit_set_in_compact_subset: "\_limit_set x \ K" and \_limit_set_in_compact_compact: "compact (\_limit_set x)" and \_limit_set_in_compact_nonempty: "\_limit_set x \ {}" and \_limit_set_in_compact_connected: "connected (\_limit_set x)" and \_limit_set_in_compact_\_limit_set_contained: "\y \ \_limit_set x. \_limit_set y \ \_limit_set x" and \_limit_set_in_compact_tendsto: "((\t. infdist (flow0 x t) (\_limit_set x)) \ 0) at_bot" using rev.\_limit_set_in_compact_subset[OF K xrev] using rev.\_limit_set_in_compact_compact[OF K xrev] using rev.\_limit_set_in_compact_nonempty[OF K xrev] using rev.\_limit_set_in_compact_connected[OF K xrev] using rev.\_limit_set_in_compact_\_limit_set_contained[OF K xrev] using rev.\_limit_set_in_compact_tendsto[OF K xrev] unfolding invariant_eq_rev \_limit_set_eq_rev existence_ivl_eq_rev flow_eq_rev0 filterlim_at_bot_mirror minus_minus . lemma \_limit_set_in_compact_existence: shows "\y. y \ \_limit_set x \ existence_ivl0 y = UNIV" using rev.\_limit_set_in_compact_existence[OF K xrev] unfolding \_limit_set_eq_rev existence_ivl_eq_rev0 by auto end end end diff --git a/thys/Poincare_Bendixson/ODE_Misc.thy b/thys/Poincare_Bendixson/ODE_Misc.thy --- a/thys/Poincare_Bendixson/ODE_Misc.thy +++ b/thys/Poincare_Bendixson/ODE_Misc.thy @@ -1,1111 +1,1111 @@ 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") (* "(\x \ {a .. b}. \ x < \ x) \ (\c\{a..b}. (\x\{a..c}. \ x \ \ x) \ (\x\{c<..b}. \ x < \ x))" (is "?th2") *) 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 by (auto simp: \l = u\) 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 sign_simps) + 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 (\x. w x * exp(-L*x)) {a0..d}" 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: sign_simps) + 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: sign_simps) + 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 "\\<^sub>F x in at_left a0. w x < 0" . moreover have "\\<^sub>F x in at_left a0. a < x" by (rule order_tendstoD) (auto intro!: \a < a0\) ultimately have "\\<^sub>F x in at_left a0. a < x \ w x < 0" by eventually_elim auto then obtain a1' where "a1'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 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: Complex_Analysis_Basics.has_derivative_mult_right mult_commute_abs) + 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 *\<^sub>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 *\<^sub>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 (force dest!: compact_imp_bounded simp: bounded_iff image_iff) + by (fastforce dest!: compact_imp_bounded simp: bounded_iff intro: that) then have "t \ {a..b} \ onorm (\i. i *\<^sub>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)" \ \TODO: use this for backwards trapped, invariant, and all assumptions\ 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: \ \TODO: when building on afp-devel (??? outdated): \<^url>\https://bitbucket.org/isa-afp/afp-devel/commits/0c3edf9248d5389197f248c723b625c419e4d3eb\\ 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: \ \TODO: when building on afp-devel: \<^url>\https://bitbucket.org/isa-afp/afp-devel/commits/0c3edf9248d5389197f248c723b625c419e4d3eb\\ 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) (* Follows from rectification *) lemma regular_locally_noteq:\ \TODO: should be true in \ll_on_open_it\\ 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)) (* By continuity of solutions and f probably *) 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<-- 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 Starlike.closed_segment_eq_real_ivl by auto + 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<--a1 > 0\ \a2 > 0\ - by (smt Diff_iff Starlike.closed_segment_eq_real_ivl atLeastAtMost_iff empty_iff half_gt_zero insert_iff pos_half_less segment(1) subset_eq) + 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) *\<^sub>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 Starlike.closed_segment_eq_real_ivl \dist t 0 < a\ by auto + 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 *\<^sub>R f x) \ norm t * (norm (f x) / 2)" by (simp add: assms(1)) then have "norm (t *\<^sub>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 *\<^sub>R f x) \ norm t * (norm (f x) / 2)" by (simp add: assms(1)) then have "norm (t *\<^sub>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) \ \TODO: there must be a more abstract argument for this, e.g., with @{thm continuous_on_closed_vimageI} and then reasoning about the connected component around 0?\ 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" "\\<^sub>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 "\\<^sub>F s' in at s. flow0 x s' \ interior M" by auto then have "\\<^sub>F s' in at_right s. flow0 x s' \ interior M" by (auto simp: eventually_at_split) moreover have "\\<^sub>F s' in at_right s. s' < t" using tendsto_ident_at \s < t\ by (rule order_tendstoD) ultimately have "\\<^sub>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 "\\<^sub>F s' in at_right s. flow0 x s' \ M" apply (rule ccontr) unfolding not_frequently proof - assume "\\<^sub>F s' in at_right s. \ flow0 x s' \ M" moreover have "\\<^sub>F s' in at_right s. s' < t" using tendsto_ident_at \s < t\ by (rule order_tendstoD) ultimately have "\\<^sub>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 simp: ) 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: \ \TODO: generalization of @{thm returns_to_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\<^sub>L (Ds (flow0 x t) o\<^sub>L flowderiv x t) o\<^sub>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\<^sub>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\<^sub>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\<^sub>L ((Ds (flow0 (fst (x, t)) (snd (x, t))) o\<^sub>L flowderiv (fst (x, t)) (snd (x, t))) o\<^sub>L embed2_blinfun) = 1\<^sub>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\<^sub>L flowderiv (fst (x, t)) (snd (x, t))) o\<^sub>L embed2_blinfun) o\<^sub>L blinfun_scaleR_left (inverse (Ds (flow0 x t)(f (flow0 x t)))) = 1\<^sub>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 /\<^sub>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\<^sub>L (Ds x o\<^sub>L flowderiv x 0) o\<^sub>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 /\<^sub>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: \ \TODO: generalizes proof of @{thm returns_to_implicit_function}!\ 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\<^sub>L (Ds (poincare_map ?P x) o\<^sub>L flowderiv x (return_time ?P x)) o\<^sub>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 \\<^sub>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}}" \ \TODO: define notion of (compact/closed)-(continuous/differentiable/C1)-surface?\ 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 (rule closed_sequentially) let ?qt = "\t. (flow0 x t - flow0 x tl) /\<^sub>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)" . \ \TODO: is this reasoning (below) with this Lipschitz constant really necessary?\ 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)) *\<^sub>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)) *\<^sub>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)) /\<^sub>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]]]\ \TODO: uuugly\ 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: sign_simps zero_less_divide_iff dist_norm pos_divide_le_eq + 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:\ \TODO: is that something more general?\ 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 "\\<^sub>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 "\\<^sub>F s in at 0. abs s < d' c" by (rule order_tendstoD tendsto_intros)+ (use d' cC in auto) moreover have "\\<^sub>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 "\\<^sub>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 "\\<^sub>F s in at 0. \x\C. dist (flow0 x s) (flow0 x 0) < e" apply eventually_elim apply (auto simp: ) 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 \ No newline at end of file diff --git a/thys/Poincare_Bendixson/Poincare_Bendixson.thy b/thys/Poincare_Bendixson/Poincare_Bendixson.thy --- a/thys/Poincare_Bendixson/Poincare_Bendixson.thy +++ b/thys/Poincare_Bendixson/Poincare_Bendixson.thy @@ -1,2824 +1,2821 @@ section \Poincare Bendixson Theory\ theory Poincare_Bendixson imports Ordinary_Differential_Equations.ODE_Analysis Analysis_Misc ODE_Misc Periodic_Orbit begin subsection \Flow to Path\ context auto_ll_on_open begin (* The path along the flow starting at time t to time t' *) definition "flow_to_path x t t' = flow0 x \ linepath t t'" lemma pathstart_flow_to_path[simp]: shows "pathstart (flow_to_path x t t') = flow0 x t" unfolding flow_to_path_def by (auto simp add: pathstart_compose) lemma pathfinish_flow_to_path[simp]: shows "pathfinish (flow_to_path x t t') = flow0 x t'" unfolding flow_to_path_def by (auto simp add: pathfinish_compose) lemma flow_to_path_unfold: shows "flow_to_path x t t' s = flow0 x ((1 - s) * t + s * t')" unfolding flow_to_path_def o_def linepath_def by auto lemma subpath0_flow_to_path: shows "(subpath 0 u (flow_to_path x t t')) = flow_to_path x t (t + u*(t'-t))" unfolding flow_to_path_def subpath_image subpath0_linepath by auto lemma path_image_flow_to_path[simp]: assumes "t \ t'" shows "path_image (flow_to_path x t t') = flow0 x ` {t..t'}" unfolding flow_to_path_def path_image_compose path_image_linepath using assms real_Icc_closed_segment by auto lemma flow_to_path_image0_right_open[simp]: assumes "t < t'" shows "flow_to_path x t t' ` {0..<1} = flow0 x `{t.. t'" assumes "{t..t'} \ existence_ivl0 x" shows "path (flow_to_path x t t')" proof - have "x \ X" using assms(1) assms(2) subset_empty by fastforce have "\xa. 0 \ xa \ xa \ 1 \ (1 - xa) * t + xa * t' \ t'" by (simp add: assms(1) convex_bound_le) moreover have "\xa. 0 \ xa \ xa \ 1 \ t \ (1 - xa) * t + xa * t'" using assms(1) by (metis add.commute add_diff_cancel_left' diff_diff_eq2 diff_le_eq mult.commute mult.right_neutral mult_right_mono right_diff_distrib') ultimately have "\xa. 0 \ xa \ xa \ 1 \ (1 - xa) * t + xa * t' \ existence_ivl0 x" using assms(2) by auto thus ?thesis unfolding path_def flow_to_path_def linepath_def by (auto intro!:continuous_intros simp add :\x \ X\) qed lemma flow_to_path_arc: assumes "t \ t'" assumes "{t..t'} \ existence_ivl0 x" assumes "\s \ {t<.. flow0 x t" assumes "flow0 x t \ flow0 x t'" shows "arc (flow_to_path x t t')" unfolding arc_def proof safe from flow_to_path_path[OF assms(1-2)] show "path (flow_to_path x t t')" . next show "inj_on (flow_to_path x t t') {0..1}" unfolding flow_to_path_def apply (rule comp_inj_on) apply (metis assms(4) inj_on_linepath) using assms path_image_linepath[of t t'] apply (auto intro!:flow0_inj_on) using flow0_inj_on greaterThanLessThan_iff linepath_image_01 real_Icc_closed_segment by fastforce qed end locale c1_on_open_R2 = c1_on_open_euclidean f f' X for f::"'a::executable_euclidean_space \ _" and f' and X + assumes dim2: "DIM('a) = 2" begin subsection \2D Line segments\ text \Line segments are specified by two endpoints The closed line segment from x to y is given by the set {x--y} and {x<-- text \ Rotates a vector clockwise 90 degrees \ definition "rot (v::'a) = (eucl_of_list [nth_eucl v 1, -nth_eucl v 0]::'a)" lemma exhaust2_nat: "(\i<(2::nat). P i) \ P 0 \ P 1" using less_2_cases by auto lemma sum2_nat: "(\i<(2::nat). P i) = P 0 + P 1" by (simp add: eval_nat_numeral) lemmas vec_simps = eucl_eq_iff[where 'a='a] dim2 eucl_of_list_eucl_nth exhaust2_nat plus_nth_eucl minus_nth_eucl uminus_nth_eucl scaleR_nth_eucl inner_nth_eucl sum2_nat algebra_simps lemma minus_expand: shows "(x::'a)-y = (eucl_of_list [x$\<^sub>e0 - y$\<^sub>e0, x$\<^sub>e1 - y$\<^sub>e1])" by (simp add:vec_simps) lemma dot_ortho[simp]: "x \ rot x = 0" unfolding rot_def minus_expand by (simp add: vec_simps) lemma nrm_dot: shows "((x::'a)-y) \ (rot (x-y)) = 0" unfolding rot_def minus_expand by (simp add: vec_simps) lemma nrm_reverse: "a \ (rot (x-y)) = - a \ (rot (y-x))" for x y::'a unfolding rot_def by (simp add:vec_simps) lemma norm_rot: "norm (rot v) = norm v" for v::'a unfolding rot_def by (simp add:vec_simps norm_nth_eucl L2_set_def) lemma rot_rot[simp]: shows "rot (rot v) = -v" unfolding rot_def by (simp add:vec_simps) lemma rot_scaleR[simp]: shows "rot ( u *\<^sub>R v) = u *\<^sub>R (rot v)" unfolding rot_def by (simp add:vec_simps) lemma rot_0[simp]: "rot 0 = 0" using rot_scaleR[of 0] by simp lemma rot_eq_0_iff[simp]: "rot x = 0 \ x = 0" apply (auto simp: rot_def) apply (metis One_nat_def norm_eq_zero norm_rot norm_zero rot_def) using rot_0 rot_def by auto lemma in_segment_inner_rot: "(x - a) \ rot (b - a) = 0" if "x \ {a--b}" proof - from that obtain u where x: "x = a + u *\<^sub>R (b - a)" "0 \ u" "u \ 1" by (auto simp: in_segment algebra_simps) show ?thesis unfolding x by (simp add: inner_add_left nrm_dot) qed lemma inner_rot_in_segment: "x \ range (\u. a + u *\<^sub>R (b - a))" if "(x - a) \ rot (b - a) = 0" "a \ b" proof - from that have x0: "b $\<^sub>e 0 = a $\<^sub>e 0 \ x $\<^sub>e 0 = (a $\<^sub>e 0 * b $\<^sub>e Suc 0 - b $\<^sub>e 0 * a $\<^sub>e Suc 0 + (b $\<^sub>e 0 - a $\<^sub>e 0) * x $\<^sub>e Suc 0) / (b $\<^sub>e Suc 0 - a $\<^sub>e Suc 0)" and x1: "b $\<^sub>e 0 \ a $\<^sub>e 0 \ x $\<^sub>e Suc 0 = ((b $\<^sub>e Suc 0 - a $\<^sub>e Suc 0) * x $\<^sub>e 0 - a $\<^sub>e 0 * b $\<^sub>e Suc 0 + b $\<^sub>e 0 * a $\<^sub>e Suc 0) / (b $\<^sub>e 0 - a $\<^sub>e 0)" by (auto simp: rot_def vec_simps divide_simps) define u where "u = (if b $\<^sub>e 0 - a $\<^sub>e 0 \ 0 then ((x $\<^sub>e 0 - a $\<^sub>e 0) / (b $\<^sub>e 0 - a $\<^sub>e 0)) else ((x $\<^sub>e 1 - a $\<^sub>e 1) / (b $\<^sub>e 1 - a $\<^sub>e 1))) " show ?thesis apply (cases "b $\<^sub>e 0 - a $\<^sub>e 0 = 0") subgoal using that(2) apply (auto intro!: image_eqI[where x="((x $\<^sub>e 1 - a $\<^sub>e 1) / (b $\<^sub>e 1 - a $\<^sub>e 1))"] simp: vec_simps x0 divide_simps algebra_simps) apply (metis ab_semigroup_mult_class.mult_ac(1) mult.commute sum_sqs_eq) by (metis mult.commute mult.left_commute sum_sqs_eq) subgoal apply (auto intro!: image_eqI[where x="((x $\<^sub>e 0 - a $\<^sub>e 0) / (b $\<^sub>e 0 - a $\<^sub>e 0))"] simp: vec_simps x1 divide_simps algebra_simps) apply (metis ab_semigroup_mult_class.mult_ac(1) mult.commute sum_sqs_eq) by (metis mult.commute mult.left_commute sum_sqs_eq) done qed lemma in_open_segment_iff_rot: "x \ {a<-- (x - a) \ rot (b - a) = 0 \ x \ (b - a) \ {a\(b - a) <..< b \ (b - a)}" if "a \ b" unfolding open_segment_line_hyperplanes[OF that] by (auto simp: nrm_dot intro!: inner_rot_in_segment) lemma in_open_segment_rotD: "x \ {a<-- (x - a) \ rot (b - a) = 0 \ x \ (b - a) \ {a\(b - a) <..< b \ (b - a)}" by (subst in_open_segment_iff_rot[symmetric]) auto lemma in_closed_segment_iff_rot: "x \ {a--b} \ (x - a) \ rot (b - a) = 0 \ x \ (b - a) \ {a\(b - a) .. b \ (b - a)}" if "a \ b" unfolding closed_segment_line_hyperplanes[OF that] using that by (auto simp: nrm_dot intro!: inner_rot_in_segment) lemma in_segment_inner_rot2: "(x - y) \ rot (a - b) = 0" if "x \ {a--b}" "y \ {a--b}" proof - from that obtain u where x: "x = a + u *\<^sub>R (b - a)" "0 \ u" "u \ 1" by (auto simp: in_segment algebra_simps) from that obtain v where y: "y = a + v *\<^sub>R (b - a)" "0 \ v" "v \ 1" by (auto simp: in_segment algebra_simps) show ?thesis unfolding x y apply (auto simp: inner_add_left ) by (smt add_diff_cancel_left' in_segment_inner_rot inner_diff_left minus_diff_eq nrm_reverse that(1) that(2) x(1) y(1)) qed lemma closed_segment_surface: "a \ b \ {a--b} = { x \ {x. x \ (b - a) \ {a\(b - a) .. b \ (b - a)}}. (x - a) \ rot (b - a) = 0}" by (auto simp: in_closed_segment_iff_rot) lemma rot_diff_commute: "rot (b - a) = -rot(a - b)" apply (auto simp: rot_def algebra_simps) by (metis One_nat_def minus_diff_eq rot_def rot_rot) subsection \Bijection Real-Complex for Jordan Curve Theorem\ definition "complex_of (x::'a) = x$\<^sub>e0 + \ * x$\<^sub>e1" definition "real_of (x::complex) = (eucl_of_list [Re x, Im x]::'a)" lemma complex_of_linear: shows "linear complex_of" unfolding complex_of_def apply (auto intro!:linearI simp add: distrib_left plus_nth_eucl) by (simp add: of_real_def scaleR_add_right scaleR_nth_eucl) lemma complex_of_bounded_linear: shows "bounded_linear complex_of" unfolding complex_of_def apply (auto intro!:bounded_linearI' simp add: distrib_left plus_nth_eucl) by (simp add: of_real_def scaleR_add_right scaleR_nth_eucl) lemma real_of_linear: shows "linear real_of" unfolding real_of_def by (auto intro!:linearI simp add: vec_simps) lemma real_of_bounded_linear: shows "bounded_linear real_of" unfolding real_of_def by (auto intro!:bounded_linearI' simp add: vec_simps) lemma complex_of_real_of: "(complex_of \ real_of) = id" unfolding complex_of_def real_of_def using complex_eq by (auto simp add:vec_simps) lemma real_of_complex_of: "(real_of \ complex_of) = id" unfolding complex_of_def real_of_def using complex_eq by (auto simp add:vec_simps) lemma complex_of_bij: shows "bij (complex_of)" using o_bij[OF real_of_complex_of complex_of_real_of] . lemma real_of_bij: shows "bij (real_of)" using o_bij[OF complex_of_real_of real_of_complex_of] . lemma real_of_inj: shows "inj (real_of)" using real_of_bij using bij_betw_imp_inj_on by auto lemma Jordan_curve_R2: fixes c :: "real \ 'a" assumes "simple_path c" "pathfinish c = pathstart c" obtains inside outside where "inside \ {}" "open inside" "connected inside" "outside \ {}" "open outside" "connected outside" "bounded inside" "\ bounded outside" "inside \ outside = {}" "inside \ outside = - path_image c" "frontier inside = path_image c" "frontier outside = path_image c" proof - from simple_path_linear_image_eq[OF complex_of_linear] have a1:"simple_path (complex_of \ c)" using assms(1) complex_of_bij using bij_betw_imp_inj_on by blast have a2:"pathfinish (complex_of \ c) = pathstart (complex_of \ c)" using assms(2) by (simp add:pathstart_compose pathfinish_compose) from Jordan_curve[OF a1 a2] obtain inside outside where io: "inside \ {}" "open inside" "connected inside" "outside \ {}" "open outside" "connected outside" "bounded inside" "\ bounded outside" "inside \ outside = {}" "inside \ outside = - path_image (complex_of \ c)" "frontier inside = path_image (complex_of \ c)" "frontier outside = path_image (complex_of \ c)" by blast let ?rin = "real_of ` inside" let ?rout = "real_of ` outside" have i: "inside = complex_of ` ?rin" using complex_of_real_of unfolding image_comp by auto have o: "outside = complex_of ` ?rout" using complex_of_real_of unfolding image_comp by auto have c: "path_image(complex_of \ c) = complex_of ` (path_image c)" by (simp add: path_image_compose) have "?rin \ {}" using io by auto moreover from open_bijective_linear_image_eq[OF real_of_linear real_of_bij] have "open ?rin" using io by auto moreover from connected_linear_image[OF real_of_linear] have "connected ?rin" using io by auto moreover have "?rout \ {}" using io by auto moreover from open_bijective_linear_image_eq[OF real_of_linear real_of_bij] have "open ?rout" using io by auto moreover from connected_linear_image[OF real_of_linear] have "connected ?rout" using io by auto moreover from bounded_linear_image[OF io(7) real_of_bounded_linear] have "bounded ?rin" . moreover from bounded_linear_image[OF _ complex_of_bounded_linear] have "\ bounded ?rout" using io(8) o by force from image_Int[OF real_of_inj] have "?rin \ ?rout = {}" using io(9) by auto moreover from bij_image_Compl_eq[OF complex_of_bij] have "?rin \ ?rout = - path_image c" using io(10) unfolding c by (metis id_apply image_Un image_comp image_cong image_ident real_of_complex_of) moreover from closure_injective_linear_image[OF real_of_linear real_of_inj] have "frontier ?rin = path_image c" using io(11) unfolding frontier_closures c by (metis \\B A. real_of ` (A \ B) = real_of ` A \ real_of ` B\ bij_image_Compl_eq c calculation(9) compl_sup double_compl io(10) real_of_bij) moreover from closure_injective_linear_image[OF real_of_linear real_of_inj] have "frontier ?rout = path_image c" using io(12) unfolding frontier_closures c by (metis \\B A. real_of ` (A \ B) = real_of ` A \ real_of ` B\ bij_image_Compl_eq c calculation(10) frontier_closures io(11) real_of_bij) ultimately show ?thesis by (meson \\ bounded (real_of ` outside)\ that) qed (* copied *) corollary Jordan_inside_outside_R2: fixes c :: "real \ 'a" assumes "simple_path c" "pathfinish c = pathstart c" shows "inside(path_image c) \ {} \ open(inside(path_image c)) \ connected(inside(path_image c)) \ outside(path_image c) \ {} \ open(outside(path_image c)) \ connected(outside(path_image c)) \ bounded(inside(path_image c)) \ \ bounded(outside(path_image c)) \ inside(path_image c) \ outside(path_image c) = {} \ inside(path_image c) \ outside(path_image c) = - path_image c \ frontier(inside(path_image c)) = path_image c \ frontier(outside(path_image c)) = path_image c" proof - obtain inner outer where *: "inner \ {}" "open inner" "connected inner" "outer \ {}" "open outer" "connected outer" "bounded inner" "\ bounded outer" "inner \ outer = {}" "inner \ outer = - path_image c" "frontier inner = path_image c" "frontier outer = path_image c" using Jordan_curve_R2 [OF assms] by blast then have inner: "inside(path_image c) = inner" by (metis dual_order.antisym inside_subset interior_eq interior_inside_frontier) have outer: "outside(path_image c) = outer" using \inner \ outer = - path_image c\ \inside (path_image c) = inner\ outside_inside \inner \ outer = {}\ by auto show ?thesis using * by (auto simp: inner outer) qed lemma jordan_points_inside_outside: fixes p :: "real \ 'a" assumes "0 < e" assumes jordan: "simple_path p" "pathfinish p = pathstart p" assumes x: "x \ path_image p" obtains y z where "y \ inside (path_image p)" "y \ ball x e" "z \ outside (path_image p)" "z \ ball x e" proof - from Jordan_inside_outside_R2[OF jordan] have xi: "x \ frontier(inside (path_image p))" and xo: "x \ frontier(outside (path_image p))" using x by auto obtain y where y:"y \ inside (path_image p)" "y \ ball x e" using \0 < e\ xi unfolding frontier_straddle by auto obtain z where z:"z \ outside (path_image p)" "z \ ball x e" using \0 < e\ xo unfolding frontier_straddle by auto show ?thesis using y z that by blast qed lemma eventually_at_open_segment: assumes "x \ {a<--\<^sub>F y in at x. (y-a) \ rot(a-b) = 0 \ y \ {a <--< b}" proof - from assms have "a \ b" by auto from assms have x: "(x - a) \ rot (b - a) = 0" "x \ (b - a) \ {a \ (b - a)<.. (b - a)}" unfolding in_open_segment_iff_rot[OF \a \ b\] by auto then have "\\<^sub>F y in at x. y \ (b - a) \ {a \ (b - a)<.. (b - a)}" by (intro topological_tendstoD) (auto intro!: tendsto_intros) then show ?thesis by eventually_elim (auto simp: in_open_segment_iff_rot[OF \a \ b\] nrm_reverse[of _ a b] algebra_simps dist_commute) qed lemma linepath_ball: assumes "x \ {a<-- 0" "ball x e \ {y. (y-a) \ rot(a-b) = 0} \ {a <--< b}" proof - from eventually_at_open_segment[OF assms] assms obtain e where "0 < e" "ball x e \ {y. (y - a) \ rot (a - b) = 0} \ {a<-- 'a" assumes jordan: "simple_path (p +++ linepath a b)" "pathfinish p = a" "pathstart p = b" assumes x: "x \ {a<-- 0" "ball x e \ path_image p = {}" "ball x e \ {y. (y-a) \ rot (a-b) > 0} \ inside (path_image (p +++ linepath a b)) \ ball x e \ {y. (y-a) \ rot (a-b) < 0} \ outside (path_image (p +++ linepath a b)) \ ball x e \ {y. (y-a) \ rot (a-b) < 0} \ inside (path_image (p +++ linepath a b)) \ ball x e \ {y. (y-a) \ rot (a-b) > 0} \ outside (path_image (p +++ linepath a b))" proof - let ?lp = "p +++ linepath a b" have "a \ b" using x by auto have pp:"path p" using jordan path_join pathfinish_linepath simple_path_imp_path by fastforce have "path_image p \ path_image (linepath a b) \ {a,b}" using jordan simple_path_join_loop_eq by (metis (no_types, lifting) inf_sup_aci(1) insert_commute path_join_path_ends path_linepath simple_path_imp_path simple_path_joinE) then have "x \ path_image p" using x unfolding path_image_linepath by (metis DiffE Int_iff le_iff_inf open_segment_def) then have "\\<^sub>F y in at x. y \ path_image p" by (intro eventually_not_in_closed) (auto simp: closed_path_image \path p\) moreover have "\\<^sub>F y in at x. (y - a) \ rot (a - b) = 0 \ y \ {a<--\<^sub>F y in at x. y \ path_image p \ ((y - a) \ rot (a - b) = 0 \ y \ {a<-- 0" "ball x e \ path_image p = {}" "ball x e \ {y. (y - a) \ rot (a - b) = 0} \ {a<--x \ path_image p\ x in_open_segment_rotD[OF x] apply (auto simp: eventually_at subset_iff dist_commute dest!: ) by (metis Int_iff all_not_in_conv dist_commute mem_ball) have a1: "pathfinish ?lp = pathstart ?lp" by (auto simp add: jordan) have "x \ path_image ?lp" using jordan(1) open_closed_segment path_image_join path_join_path_ends simple_path_imp_path x by fastforce from jordan_points_inside_outside[OF e(1) jordan(1) a1 this] obtain y z where y: "y \ inside (path_image ?lp)" "y \ ball x e" and z: "z \ outside (path_image ?lp)" "z \ ball x e" by blast have jordancurve: "inside (path_image ?lp) \ outside(path_image ?lp) = {}" "frontier (inside (path_image ?lp)) = path_image ?lp" "frontier (outside (path_image ?lp)) = path_image ?lp" using Jordan_inside_outside_R2[OF jordan(1) a1] by auto define b1 where "b1 = ball x e \ {y. (y-a) \ rot (a-b) > 0}" define b2 where "b2 = ball x e \ {y. (y-a) \ rot (a-b) < 0}" define b3 where "b3 = ball x e \ {y. (y-a) \ rot (a-b) = 0}" have "path_connected b1" unfolding b1_def apply (auto intro!: convex_imp_path_connected convex_Int simp add:inner_diff_left) using convex_halfspace_gt[of "a \ rot (a - b)" "rot(a-b)"] inner_commute by (metis (no_types, lifting) Collect_cong) have "path_connected b2" unfolding b2_def apply (auto intro!: convex_imp_path_connected convex_Int simp add:inner_diff_left) using convex_halfspace_lt[of "rot(a-b)" "a \ rot (a - b)"] inner_commute by (metis (no_types, lifting) Collect_cong) have "b1 \ path_image(linepath a b) = {}" unfolding path_image_linepath b1_def using closed_segment_surface[OF \a \ b\] in_segment_inner_rot2 by auto then have b1i:"b1 \ path_image ?lp = {}" by (metis IntD2 b1_def disjoint_iff_not_equal e(2) inf_sup_aci(1) not_in_path_image_join) have "b2 \ path_image(linepath a b) = {}" unfolding path_image_linepath b2_def using closed_segment_surface[OF \a \ b\] in_segment_inner_rot2 by auto then have b2i:"b2 \ path_image ?lp = {}" by (metis IntD2 b2_def disjoint_iff_not_equal e(2) inf_sup_aci(1) not_in_path_image_join) have bsplit: "ball x e = b1 \ b2 \ b3" unfolding b1_def b2_def b3_def by auto have "z \ b3" proof clarsimp assume "z \ b3" then have "z \ {a<-- path_image(linepath a b)" by (auto simp add: open_segment_def) then have "z \ path_image ?lp" by (simp add: jordan(2) path_image_join) thus False using z using inside_Un_outside by fastforce qed then have z12: "z \ b1 \ z \ b2" using z bsplit by blast have "y \ b3" proof clarsimp assume "y \ b3" then have "y \ {a<-- path_image(linepath a b)" by (auto simp add: open_segment_def) then have "y \ path_image ?lp" by (simp add: jordan(2) path_image_join) thus False using y using inside_Un_outside by fastforce qed then have "y \ b1 \ y \ b2" using y bsplit by blast moreover { assume "y \ b1" then have "b1 \ inside (path_image ?lp) \ {}" using y by blast from path_connected_not_frontier_subset[OF \path_connected b1\ this] have 1:"b1 \ inside (path_image ?lp)" unfolding jordancurve using b1i by blast then have "z \ b2" using jordancurve(1) z(1) z12 by blast then have "b2 \ outside (path_image ?lp) \ {}" using z by blast from path_connected_not_frontier_subset[OF \path_connected b2\ this] have 2:"b2 \ outside (path_image ?lp)" unfolding jordancurve using b2i by blast note conjI[OF 1 2] } moreover { assume "y \ b2" then have "b2 \ inside (path_image ?lp) \ {}" using y by blast from path_connected_not_frontier_subset[OF \path_connected b2\ this] have 1:"b2 \ inside (path_image ?lp)" unfolding jordancurve using b2i by blast then have "z \ b1" using jordancurve(1) z(1) z12 by blast then have "b1 \ outside (path_image ?lp) \ {}" using z by blast from path_connected_not_frontier_subset[OF \path_connected b1\ this] have 2:"b1 \ outside (path_image ?lp)" unfolding jordancurve using b1i by blast note conjI[OF 1 2] } ultimately show ?thesis unfolding b1_def b2_def using that[OF e(1-2)] by auto qed subsection \Transversal Segments\\ \TODO: Transversal surface in Euclidean space?!\ definition "transversal_segment a b \ a \ b \ {a--b} \ X \ (\z \ {a--b}. f z \ rot (a-b) \ 0)" lemma transversal_segment_reverse: assumes "transversal_segment x y" shows "transversal_segment y x" unfolding transversal_segment_def by (metis (no_types, hide_lams) add.left_neutral add_uminus_conv_diff assms closed_segment_commute inner_diff_left inner_zero_left nrm_reverse transversal_segment_def) lemma transversal_segment_commute: "transversal_segment x y \ transversal_segment y x" using transversal_segment_reverse by blast lemma transversal_segment_neg: assumes "transversal_segment x y" assumes w: "w \ {x -- y}" and "f w \ rot (x-y) < 0" shows "\z \ {x--y}. f(z) \ rot (x-y) < 0" proof (rule ccontr) assume " \ (\z\{x--y}. f z \ rot (x-y) < 0)" then obtain z where z: "z \ {x--y}" "f z \ rot (x-y) \ 0" by auto define ff where "ff = (\s. f (w + s *\<^sub>R (z - w)) \ rot (x-y))" have f0:"ff 0 \ 0" unfolding ff_def using assms(3) by simp have fu:"ff 1 \ 0" by (auto simp: ff_def z) from assms(2) obtain u where u: "0 \ u" "u \ 1" "w = (1 - u) *\<^sub>R x + u *\<^sub>R y" unfolding in_segment by blast have "{x--y} \ X" using assms(1) unfolding transversal_segment_def by blast then have "continuous_on {0..1} ff" unfolding ff_def using assms(2) by (auto intro!:continuous_intros closed_subsegmentI z elim!: set_mp) from IVT'[of ff, OF f0 fu zero_le_one this] obtain s where s: "s \ 0" "s \ 1" "ff s = 0" by blast have "w + s *\<^sub>R (z - w) \ {x -- y}" by (auto intro!: closed_subsegmentI z s w) with \ff s = 0\ show False using s assms(1) unfolding transversal_segment_def ff_def by blast qed lemmas transversal_segment_sign_less = transversal_segment_neg[OF _ ends_in_segment(1)] lemma transversal_segment_pos: assumes "transversal_segment x y" assumes w: "w \ {x -- y}" "f w \ rot (x-y) > 0" shows "\z \ {x--y}. f(z) \ rot (x-y) > 0" using transversal_segment_neg[OF transversal_segment_reverse[OF assms(1)], of w] w by (auto simp: rot_diff_commute[of x y] closed_segment_commute) lemma transversal_segment_posD: assumes "transversal_segment x y" and pos: "z \ {x -- y}" "f z \ rot (x - y) > 0" shows "x \ y" "{x--y} \ X" "\z. z \ {x--y} \ f z \ rot (x-y) > 0" using assms(1) transversal_segment_pos[OF assms] by (auto simp: transversal_segment_def) lemma transversal_segment_negD: assumes "transversal_segment x y" and pos: "z \ {x -- y}" "f z \ rot (x - y) < 0" shows "x \ y" "{x--y} \ X" "\z. z \ {x--y} \ f z \ rot (x-y) < 0" using assms(1) transversal_segment_neg[OF assms] by (auto simp: transversal_segment_def) lemma transversal_segmentE: assumes "transversal_segment x y" obtains "x \ y" "{x -- y} \ X" "\z. z \ {x--y} \ f z \ rot (x - y) > 0" | "x \ y" "{x -- y} \ X" "\z. z \ {x--y} \ f z \ rot (y - x) > 0" proof (cases "f x \ rot (x - y) < 0") case True from transversal_segment_negD[OF assms ends_in_segment(1) True] have "x \ y" "{x -- y} \ X" "\z. z \ {x--y} \ f z \ rot (y - x) > 0" by (auto simp: rot_diff_commute[of x y]) then show ?thesis .. next case False then have "f x \ rot (x - y) > 0" using assms - by (auto simp: transversal_segment_def sign_simps not_less order.order_iff_strict) + by (auto simp: transversal_segment_def algebra_split_simps not_less order.order_iff_strict) from transversal_segment_posD[OF assms ends_in_segment(1) this] show ?thesis .. qed lemma dist_add_vec: shows "dist (x + s *\<^sub>R v) x = abs s * norm v" by (simp add: dist_cancel_add1) lemma transversal_segment_exists: assumes "x \ X" "f x \ 0" obtains a b where "x \ {a<--s::real. x + (s/norm(f x)) *\<^sub>R rot (f x))" have "norm (f x) > 0" using assms(2) using zero_less_norm_iff by blast then have distl: "\s. dist (l s) x = abs s" unfolding l_def dist_add_vec by (auto simp add: norm_rot) obtain d where d:"d > 0" "cball x d \ X" by (meson UNIV_I assms(1) local.local_unique_solution) then have lb: "l`{-d..d} \ cball x d" using distl by (simp add: abs_le_iff dist_commute image_subset_iff) from fcontx[OF assms(1)] have "continuous (at x) f" . then have c:"continuous (at 0) ((\y. (f y \ f x)) \ l)" unfolding l_def by (auto intro!:continuous_intros simp add: assms(2)) have "((\y. f y \ f x) \ l) 0 > 0" using assms(2) unfolding l_def o_def by auto from continuous_at_imp_cball[OF c this] obtain r where r:"r > 0" " \z\cball 0 r. 0 < ((\y. f y \ f x) \ l) z" by blast then have rc:"\z \ l`{-r..r}. 0 < f z \ f x" using real_norm_def by auto define dr where "dr = min r d" have t1:"l (-dr) \ l dr" unfolding l_def dr_def by (smt \0 < d\ \0 < norm (f x)\ \0 < r\ add_left_imp_eq divide_cancel_right norm_rot norm_zero scale_cancel_right) have "x = midpoint (l (-dr)) (l dr)" unfolding midpoint_def l_def by auto then have xin:"x \ {l (-dr)<--<(l dr)}" using t1 by auto (* TODO: actually this should be equality, but l is affine ... also the existing stuff about -- is a little too specific *) have lsub:"{l (-dr)--l dr} \ l`{-dr..dr}" proof safe fix z assume "z \ {l (- dr)--l dr}" then obtain u where u: "0 \ u" "u \ 1" "z = (1 - u) *\<^sub>R (l (-dr)) + u *\<^sub>R (l dr)" unfolding in_segment by blast then have "z = x - (1-u) *\<^sub>R (dr/norm(f x)) *\<^sub>R rot (f x) + u *\<^sub>R (dr/norm(f x)) *\<^sub>R rot (f x) " unfolding l_def by (simp add: l_def scaleR_add_right scale_right_diff_distrib u(3)) also have "... = x - (1 - 2 * u) *\<^sub>R (dr/norm(f x)) *\<^sub>R rot (f x)" by (auto simp add: algebra_simps divide_simps simp flip: scaleR_add_left) also have "... = x + (((2 * u - 1) * dr)/norm(f x)) *\<^sub>R rot (f x)" by (smt add_uminus_conv_diff scaleR_scaleR scale_minus_left times_divide_eq_right) finally have zeq: "z = l ((2*u-1)*dr)" unfolding l_def . have ub: " 2* u - 1 \ 1 \ -1 \ 2* u - 1 " using u by linarith thus "z \ l ` {- dr..dr}" using zeq by (smt atLeastAtMost_iff d(1) dr_def image_eqI mult.commute mult_left_le mult_minus_left r(1)) qed have t2: "{l (- dr)--l dr} \ X" using lsub by (smt atLeastAtMost_iff d(2) dist_commute distl dr_def image_subset_iff mem_cball order_trans) have "l (- dr) - l dr = -2 *\<^sub>R (dr/norm(f x)) *\<^sub>R rot (f x)" unfolding l_def by (simp add: algebra_simps flip: scaleR_add_left) then have req: "rot (l (- dr) - l dr) = (2 * dr/norm(f x)) *\<^sub>R f x" by auto (metis add.inverse_inverse rot_rot rot_scaleR) have "l`{-dr..dr} \ l ` {-r ..r}" by (simp add: dr_def image_mono) then have "{l (- dr)--l dr} \ l ` {-r .. r}" using lsub by auto then have "\z \ {l (- dr)--l dr}. 0 < f z \ f x" using rc by blast moreover have "(dr / norm (f x)) > 0" using \0 < norm (f x)\ d(1) dr_def r(1) by auto ultimately have t3: "\z \ {l (- dr)--l dr}. f z \ rot (l (- dr)- l dr) > 0" unfolding req by (smt divide_divide_eq_right inner_scaleR_right mult_2 norm_not_less_zero scaleR_2 times_divide_eq_left times_divide_eq_right zero_less_divide_iff) have "transversal_segment (l (-dr)) (l dr)" using t1 t2 t3 unfolding transversal_segment_def by auto thus ?thesis using xin using that by auto qed text \Perko Section 3.7 Lemma 2 part 1.\ lemma flow_transversal_segment_finite_intersections: assumes "transversal_segment a b" assumes "t \ t'" "{t .. t'} \ existence_ivl0 x" shows "finite {s\{t..t'}. flow0 x s \ {a--b}}" proof - from assms have "a \ b" by (simp add: transversal_segment_def) show ?thesis unfolding closed_segment_surface[OF \a \ b\] apply (rule flow_transversal_surface_finite_intersections[where Ds="\_. blinfun_inner_left (rot (b - a))"]) by (use assms in \auto intro!: closed_Collect_conj closed_halfspace_component_ge closed_halfspace_component_le derivative_eq_intros simp: transversal_segment_def nrm_reverse[where x=a] in_closed_segment_iff_rot\) qed lemma transversal_bound_posE: assumes transversal: "transversal_segment a b" assumes direction: "z \ {a -- b}" "f z \ (rot (a - b)) > 0" obtains d B where "d > 0" "0 < B" "\x y. x \ {a -- b} \ dist x y \ d \ f y \ (rot (a - b)) \ B" proof - let ?a = "(\y. (f y) \ (rot (a - b)))" from transversal_segment_posD[OF transversal direction] have seg: "a \ b" "{a--b} \ X" "z \ {a--b} \ 0 < f z \ rot (a - b)" for z by auto { fix x assume "x \ {a--b}" then have "x \ X" "f x \ 0" "a \ b" using transversal by (auto simp: transversal_segment_def) then have "?a \x\ ?a x" by (auto intro!: tendsto_eq_intros) moreover have "?a x > 0" using seg \x \ {a -- b}\ \f x \ 0\ by (auto simp: simp del: divide_const_simps intro!: divide_pos_pos mult_pos_pos) ultimately have "\\<^sub>F x in at x. ?a x > 0" by (rule order_tendstoD) moreover have "\\<^sub>F x in at x. x \ X" by (rule topological_tendstoD[OF tendsto_ident_at open_dom \x \ X\]) moreover have "\\<^sub>F x in at x. f x \ 0" by (rule tendsto_imp_eventually_ne tendsto_intros \x \ X\ \f x \ 0\)+ ultimately have "\\<^sub>F x in at x. ?a x>0 \ x \ X \ f x \ 0" by eventually_elim auto then obtain d where d: "0 < d" "\y. y \ cball x d \ ?a y > 0 \ y \ X \ f y \ 0" using \?a x > 0\ \x \ X\ by (force simp: eventually_at_le dist_commute) have "continuous_on (cball x d) ?a" using d \a \ b\ by (auto intro!: continuous_intros) from compact_continuous_image[OF this compact_cball] have "compact (?a ` cball x d)" . from compact_attains_inf[OF this] obtain s where "s \ cball x d" "\x\cball x d. ?a x \ ?a s" using \d > 0\ by auto then have "\d>0. \b>0. \x \ cball x d. ?a x \ b" using d by (force simp: intro: exI[where x="?a s"]) } then obtain dx Bx where dB: "\x y. x \ {a -- b} \ y\cball x (dx x) \ ?a y \ Bx x" "\x. x \ {a -- b} \ Bx x > 0" "\x. x \ {a -- b} \ dx x > 0" by metis define d' where "d' = (\x. dx x / 2)" have d': "\x. x \ {a -- b} \ \y\cball x (d' x). ?a y \ Bx x" "\x. x \ {a -- b} \ d' x > 0" using dB(1,3) by (force simp: d'_def)+ have d'B: "\x. x \ {a -- b} \ \y\cball x (d' x). ?a y \ Bx x" using d' by auto have "{a--b} \ \((\x. ball x (d' x)) ` {a -- b})" using d'(2) by auto from compactE_image[OF compact_segment _ this] obtain X where X: "X \ {a--b}" and [simp]: "finite X" and cover: "{a--b} \ (\x\X. ball x (d' x))" by auto have [simp]: "X \ {}" using X cover by auto define d where "d = Min (d' ` X)" define B where "B = Min (Bx ` X)" have "d > 0" using X d' by (auto simp: d_def d'_def) moreover have "B > 0" using X dB by (auto simp: B_def simp del: divide_const_simps) moreover have "B \ ?a y" if "x \ {a -- b}" "dist x y \ d" for x y proof - from \x \ {a -- b}\ obtain xc where xc: "xc \ X" "x \ ball xc (d' xc)" using cover by auto have "?a y \ Bx xc" proof (rule dB) show "xc \ {a -- b}" using xc \X \ _\ by auto have "dist xc y \ dist xc x + dist x y" by norm also have "dist xc x \ d' xc" using xc by auto also note \dist x y \ d\ also have "d \ d' xc" using xc by (auto simp: d_def) also have "d' xc + d' xc = dx xc" by (simp add: d'_def) finally show "y \ cball xc (dx xc)" by simp qed also have "B \ Bx xc" using xc unfolding B_def by (auto simp: B_def) finally (xtrans) show ?thesis . qed ultimately show ?thesis .. qed lemma transversal_bound_negE: assumes transversal: "transversal_segment a b" assumes direction: "z \ {a -- b}" "f z \ (rot (a - b)) < 0" obtains d B where "d > 0" "0 < B" "\x y. x \ {a -- b} \ dist x y \ d \ f y \ (rot (b - a)) \ B" proof - from direction have "z \ {b -- a}" "f z \ (rot (b - a)) > 0" by (auto simp: closed_segment_commute rot_diff_commute[of b a]) from transversal_bound_posE[OF transversal_segment_reverse[OF transversal] this] obtain d B where "d > 0" "0 < B" "\x y. x \ {a -- b} \ dist x y \ d \ f y \ (rot (b - a)) \ B" by (auto simp: closed_segment_commute) then show ?thesis .. qed lemma leaves_transversal_segmentE: assumes transversal: "transversal_segment a b" obtains T n where "T > 0" "n = a - b \ n = b - a" "\x. x \ {a -- b} \ {-T..T} \ existence_ivl0 x" "\x s. x \ {a -- b} \ 0 < s \ s \ T \ (flow0 x s - x) \ rot n > 0" "\x s. x \ {a -- b} \ -T \ s \ s < 0 \ (flow0 x s - x) \ rot n < 0" proof - from transversal_segmentE[OF assms(1)] obtain n where n: "n = (a - b) \ n = (b - a)" and seg: "a \ b" "{a -- b} \ X" "\z. z \ {a--b} \ f z \ rot n > 0" by metis from open_existence_ivl_on_compact[OF \{a -- b} \ X\] obtain t where "0 < t" and t: "x \ {a--b} \ {- t..t} \ existence_ivl0 x" for x by auto from n obtain d B where B: "0 < d" "0 < B" "(\x y. x \ {a--b} \ dist x y \ d \ B \ f y \ rot n)" proof assume n_def: "n = a - b" with seg have pos: "0 < f a \ rot (a - b)" by auto from transversal_bound_posE[OF transversal ends_in_segment(1) pos, folded n_def] show ?thesis using that by blast next assume n_def: "n = b - a" with seg have pos: "0 > f a \ rot (a - b)" by (auto simp: rot_diff_commute[of a b]) from transversal_bound_negE[OF transversal ends_in_segment(1) this, folded n_def] show ?thesis using that by blast qed define S where "S = \((\x. ball x d) ` {a -- b})" have S: "x \ S \ B \ f x \ rot n" for x by (auto simp: S_def intro!: B) have "open S" by (auto simp: S_def) have "{a -- b} \ S" by (auto simp: S_def \0 < d\) have "\\<^sub>F (t, x) in at (0, x). flow0 x t \ S" if "x \ {a -- b}" for x unfolding split_beta' apply (rule topological_tendstoD tendsto_intros)+ using set_mp[OF \{a -- b} \ X\ that] \0 < d\ that \open S\ \{a -- b} \ S\ by (force simp: )+ then obtain d' where d': "\x. x \ {a--b} \ d' x > 0" "\x y s. x \ {a--b} \ (s = 0 \ y \ x) \ dist (s, y) (0, x) < d' x \ flow0 y s \ S" by (auto simp: eventually_at) metis define d2 where "d2 x = d' x / 2" for x have d2: "\x. x \ {a--b} \ d2 x > 0" using d' by (auto simp: d2_def) have C: "{a--b} \ \((\x. ball x (d2 x)) ` {a -- b})" using d2 by auto from compactE_image[OF compact_segment _ C] obtain C' where "C' \ {a--b}" and [simp]: "finite C'" and C'_cover: "{a--b} \ (\c\C'. ball c (d2 c))" by auto define T where "T = Min (insert t (d2 ` C'))" have "T > 0" using \0 < t\ d2 \C' \ _\ by (auto simp: T_def) moreover note n moreover have T_ex: "{-T..T} \ existence_ivl0 x" if "x \ {a--b}" for x by (rule order_trans[OF _ t[OF that]]) (auto simp: T_def) moreover have B_le: "B \ f (flow0 x \) \ rot n" if "x \ {a -- b}" and c': "c' \ C'" "x \ ball c' (d2 c')" and "\ \ 0" and \_le: "\\\ < d2 c'" for x c' \ proof - have "c' \ {a -- b}" using c' \C' \ _\ by auto moreover have "\ = 0 \ x \ c'" using \\ \ 0\ by simp moreover have "dist (\, x) (0, c') < d' c'" proof - have "dist (\, x) (0, c') \ dist (\, x) (\, c') + dist (\, c') (0, c')" by norm also have "dist (\, x) (\, c') < d2 c'" using c' by (simp add: dist_prod_def dist_commute) also have "T \ d2 c'" using c' by (auto simp: T_def) then have "dist (\, c') (0, c') < d2 c'" using \_le by (simp add: dist_prod_def) also have "d2 c' + d2 c' = d' c'" by (simp add: d2_def) finally show ?thesis by simp qed ultimately have "flow0 x \ \ S" by (rule d') then show ?thesis by (rule S) qed let ?g = "(\x t. (flow0 x t - x) \ rot n)" have cont: "continuous_on {-T .. T} (?g x)" if "x \ {a--b}" for x using T_ex that by (force intro!: continuous_intros) have deriv: "-T \ s' \ s' \ T \ ((?g x) has_derivative (\t. t * (f (flow0 x s') \ rot n))) (at s')" if "x \ {a--b}" for x s' using T_ex that by (force intro!: derivative_eq_intros simp: flowderiv_def blinfun.bilinear_simps) have "(flow0 x s - x) \ rot n > 0" if "x \ {a -- b}" "0 < s" "s \ T" for x s proof (rule ccontr, unfold not_less) have [simp]: "x \ X" using that \{a -- b} \ X\ by auto assume H: "(flow0 x s - x) \ rot n \ 0" have cont: "continuous_on {0 .. s} (?g x)" using cont by (rule continuous_on_subset) (use that in auto) from mvt[OF \0 < s\ cont deriv] that obtain \ where \: "0 < \" "\ < s" "(flow0 x s - x) \ rot n = s * (f (flow0 x \) \ rot n)" by (auto intro: continuous_on_subset) note \0 < B\ also from C'_cover that obtain c' where c': "c' \ C'" "x \ ball c' (d2 c')" by auto have "B \ f (flow0 x \) \ rot n" proof (rule B_le[OF that(1) c']) show "\ \ 0" using \0 < \\ by simp have "T \ d2 c'" using c' by (auto simp: T_def) then show "\\\ < d2 c'" using \0 < \\ \\ < s\ \s \ T\ by (simp add: dist_prod_def) qed also from \ H have "\ \ 0" - by (auto simp add: sign_simps not_less split: if_splits) - (metis mult_zero_right real_mult_le_cancel_iff2 that(2)) + by (auto simp add: algebra_split_simps not_less split: if_splits) finally show False by simp qed moreover have "(flow0 x s - x) \ rot n < 0" if "x \ {a -- b}" "-T \ s" "s < 0" for x s proof (rule ccontr, unfold not_less) have [simp]: "x \ X" using that \{a -- b} \ X\ by auto assume H: "(flow0 x s - x) \ rot n \ 0" have cont: "continuous_on {s .. 0} (?g x)" using cont by (rule continuous_on_subset) (use that in auto) from mvt[OF \s < 0\ cont deriv] that obtain \ where \: "s < \" "\ < 0" "(flow0 x s - x) \ rot n = s * (f (flow0 x \) \ rot n)" by auto note \0 < B\ also from C'_cover that obtain c' where c': "c' \ C'" "x \ ball c' (d2 c')" by auto have "B \ (f (flow0 x \) \ rot n)" proof (rule B_le[OF that(1) c']) show "\ \ 0" using \0 > \\ by simp have "T \ d2 c'" using c' by (auto simp: T_def) then show "\\\ < d2 c'" using \0 > \\ \\ > s\ \s \ - T\ by (simp add: dist_prod_def) qed also from \ H have "\ \ 0" - by (simp add: sign_simps algebra_simps) - (metis less_eq_real_def mult_less_cancel_left mult_pos_neg2 mult_zero_right that(3)) + by (simp add: algebra_split_simps) finally show False by simp qed ultimately show ?thesis .. qed lemma inner_rot_pos_move_base: "(x - a) \ rot (a - b) > 0" if "(x - y) \ rot (a - b) > 0" "y \ {a -- b}" by (smt in_segment_inner_rot inner_diff_left inner_minus_right minus_diff_eq rot_rot that) lemma inner_rot_neg_move_base: "(x - a) \ rot (a - b) < 0" if "(x - y) \ rot (a - b) < 0" "y \ {a -- b}" by (smt in_segment_inner_rot inner_diff_left inner_minus_right minus_diff_eq rot_rot that) lemma inner_pos_move_base: "(x - a) \ n > 0" if "(a - b) \ n = 0" "(x - y) \ n > 0" "y \ {a -- b}" proof - from that(3) obtain u where y_def: "y = (1 - u) *\<^sub>R a + u *\<^sub>R b" and u: "0 \ u" "u \ 1" by (auto simp: in_segment) have "(x - a) \ n = (x - y) \ n - u * ((a - b) \ n)" by (simp add: algebra_simps y_def) also have "\ = (x - y) \ n" by (simp add: that) also note \\ > 0\ finally show ?thesis . qed lemma inner_neg_move_base: "(x - a) \ n < 0" if "(a - b) \ n = 0" "(x - y) \ n < 0" "y \ {a -- b}" proof - from that(3) obtain u where y_def: "y = (1 - u) *\<^sub>R a + u *\<^sub>R b" and u: "0 \ u" "u \ 1" by (auto simp: in_segment) have "(x - a) \ n = (x - y) \ n - u * ((a - b) \ n)" by (simp add: algebra_simps y_def) also have "\ = (x - y) \ n" by (simp add: that) also note \\ < 0\ finally show ?thesis . qed lemma rot_same_dir: assumes "x1 \ {a<-- {x1<-- rot (a-b) > 0) = (y \ rot(x1-x2) > 0)" "(y \ rot (a-b) < 0) = (y \ rot(x1-x2) < 0)" using oriented_subsegment_scale[OF assms] apply (smt inner_scaleR_right nrm_reverse rot_scaleR zero_less_mult_iff) by (smt \\thesis. (\e. \0 < e; b - a = e *\<^sub>R (x2 - x1)\ \ thesis) \ thesis\ inner_minus_right inner_scaleR_right rot_diff_commute rot_scaleR zero_less_mult_iff) subsection \Monotone Step Lemma\ lemma flow0_transversal_segment_monotone_step: assumes "transversal_segment a b" assumes "t1 \ t2" "{t1..t2} \ existence_ivl0 x" assumes x1: "flow0 x t1 \ {a<-- {flow0 x t1<--t. t \ {t1<.. flow0 x t \ {a<-- t2" "t \ existence_ivl0 x" shows "flow0 x t \ {a<--{t1..t2} \ existence_ivl0 x\ note t1t2 = \\t. t \ {t1<.. flow0 x t \ {a<-- (* Basic properties of the segment *) have x1neqx2: "flow0 x t1 \ flow0 x t2" using open_segment_def x2 by force then have t1neqt2: "t1 \ t2" by auto have [simp]: "a \ b" and \{a -- b} \ X\ using \transversal_segment a b\ by (auto simp: transversal_segment_def) from x1 obtain i1 where i1: "flow0 x t1 = line a b i1" "0 < i1" "i1 < 1" by (auto simp: in_open_segment_iff_line) from x2 obtain i2 where i2: "flow0 x t2 = line a b i2" "0 < i1" "i1 < i2" by (auto simp: i1 line_open_segment_iff) have "{a <--< flow0 x t1} \ {a<-- {a<-- {flow0 x t1 <-- {a <-- {a <--< flow0 x t2}" using x1 x2 by (simp add: open_closed_segment subset_open_segment x2) then have subl2: "{flow0 x t1-- {a <--< flow0 x t2}" using x1 x2 by (smt DiffE DiffI \flow0 x t1 \ {a<-- half_open_segment_def insert_iff open_segment_def subset_eq) have sub1b: "{flow0 x t1--b} \ {a--b}" by (simp add: open_closed_segment subset_closed_segment x1) have suba2: "{a--flow0 x t2} \ {a -- b}" using open_closed_segment subset_closed_segment t12sub by blast then have suba2o: "{a<-- {a -- b}" using open_closed_segment subset_closed_segment t12sub by blast have x2_notmem: "flow0 x t2 \ {a--flow0 x t1}" using i1 i2 by (auto simp: closed_segment_line_iff) have suba12: "{a--flow0 x t1} \ {a--flow0 x t2}" by (simp add: \flow0 x t1 \ {a<-- open_closed_segment subset_closed_segment) then have suba12_open: "{a<-- {a<-- {a--b}" using suba2 by auto have intereq: "\t. t1 \ t \ t \ t2 \ flow0 x t \ {a<-- t = t1 \ t = t2" proof (rule ccontr) fix t assume t: "t1 \ t" "t \ t2" "flow0 x t \ {a<--(t= t1 \ t = t2)" then have "t \ {t1<.. {a<--t. t1 \ t \ t \ t2 \ flow0 x t \ {flow0 x t1--flow0 x t2} \ t = t1 \ t = t2" using t12sub by blast (* The Jordan curve *) define J1 where "J1 = flow_to_path x t1 t2" define J2 where "J2 = linepath (flow0 x t2) (flow0 x t1)" define J where "J = J1 +++ J2" (* Proof that J is a Jordan curve *) have "pathfinish J = pathstart J" unfolding J_def J1_def J2_def by (auto simp add: pathstart_compose pathfinish_compose) have piJ: "path_image J = path_image J1 \ path_image J2" unfolding J_def J1_def J2_def apply (rule path_image_join) by auto have "flow0 x t1 \ flow0 x ` {t1..t2} \ flow0 x t2 \ flow0 x ` {t1..t2}" using atLeastAtMost_iff \t1 \ t2\ by blast then have piD: "path_image J = path_image J1 \ {flow0 x t1 <--t1 \ t2\] path_image_linepath open_segment_def by (smt Diff_idemp Diff_insert2 Un_Diff_cancel closed_segment_commute mk_disjoint_insert) have "\s\{t1<.. flow0 x t1" using x1 t1t2 by fastforce from flow_to_path_arc[OF \t1 \ t2\ exist this x1neqx2] have "arc J1" using J1_def assms flow_to_path_arc by auto then have "simple_path J" unfolding J_def using \arc J1\ J1_def J2_def assms x1neqx2 t1neqt2 apply (auto intro!:simple_path_join_loop) using intereqt12 closed_segment_commute by blast from Jordan_inside_outside_R2[OF this \pathfinish J = pathstart J\] obtain inner outer where inner_def: "inner = inside (path_image J)" and outer_def: "outer = outside (path_image J)" and io: "inner \ {}" "open inner" "connected inner" "outer \ {}" "open outer" "connected outer" "bounded inner" "\ bounded outer" "inner \ outer = {}" "inner \ outer = - path_image J" "frontier inner = path_image J" "frontier outer = path_image J" by metis from io have io2: "outer \ inner = {}" "outer \ inner = - path_image J" by auto have swap_side: "\y t. y \ side2 \ 0 \ t \ t \ existence_ivl0 y \ flow0 y t \ closure side1 \ \T. 0 < T \ T \ t \ (\s \{0.. side2) \ flow0 y T \ {flow0 x t1-- side2 = {}" "open side2" "frontier side1 = path_image J" "frontier side2 = path_image J" "side1 \ side2 = - path_image J" for side1 side2 proof - fix y t assume yt: "y \ side2" "0 \ t" "t \ existence_ivl0 y" "flow0 y t \ closure side1" define fp where "fp = flow_to_path y 0 t" have ex:"{0..t} \ existence_ivl0 y" using ivl_subset_existence_ivl yt(3) by blast then have y0:"flow0 y 0 = y" using mem_existence_ivl_iv_defined(2) yt(3) by auto then have tpos: "t > 0" using yt(2) \side1 \ side2 = {}\ using yt(1) yt(4) by (metis closure_iff_nhds_not_empty less_eq_real_def order_refl that(2)) from flow_to_path_path[OF yt(2) ex] have a1: "path fp" unfolding fp_def . have "y \ closure side2" using yt(1) by (simp add: assms closure_def) then have a2: "pathstart fp \ closure side2" unfolding fp_def using y0 by auto have a3:"pathfinish fp \ side2" using yt(4) \side1 \ side2 = {}\ unfolding fp_def apply auto using closure_iff_nhds_not_empty that(2) by blast from subpath_to_frontier_strong[OF a1 a3] obtain u where u:"0 \ u" "u \ 1" "fp u \ interior side2" "u = 0 \ (\x. 0 \ x \ x < 1 \ subpath 0 u fp x \ interior side2) \ fp u \ closure side2" by blast have p1:"path_image (subpath 0 u fp) = flow0 y ` {0 .. u*t}" unfolding fp_def subpath0_flow_to_path using path_image_flow_to_path by (simp add: u(1) yt(2)) have p2:"fp u = flow0 y (u*t)" unfolding fp_def flow_to_path_unfold by simp have inout:"interior side2 = side2" using \open side2\ by (simp add: interior_eq) then have iemp: "side2 \ path_image J = {}" using \frontier side2 = path_image J\ by (metis frontier_disjoint_eq inf_sup_aci(1) interior_eq) have "u \ 0" using inout u(3) y0 p2 yt(1) by force then have c1:"u * t > 0" using tpos u y0 \side1 \ side2 = {}\ using frontier_disjoint_eq io(5) yt(1) zero_less_mult_iff by fastforce have uim:"fp u \ path_image J" using u \u \ 0\ using \frontier side2 = path_image J\ by (metis ComplI IntI closure_subset frontier_closures inout subsetD) have c2:"u * t \ t" using u(1-2) tpos by auto have"(flow_to_path y 0 (u * t) ` {0..<1} \ side2)" using \u \ 0\ u inout unfolding fp_def subpath0_flow_to_path by auto then have c3:"\s \{0.. side2" by auto have c4: "flow0 y (u*t) \ path_image J" using uim path_image_join_subset by (simp add: p2) have "flow0 y (u*t) \ path_image J1 \ flow0 y (u*t) = flow0 x t1" proof clarsimp assume "flow0 y (u*t) \ path_image J1" then obtain s where s: "t1 \ s" "s \ t2" "flow0 x s = flow0 y (u*t)" using J1_def \t1 \ t2\ by auto have "s = t1" proof (rule ccontr) assume "s \ t1" then have st1:"s > t1" using s(1) by linarith define sc where "sc = min (s-t1) (u*t)" have scd: "s-sc \ {t1..t2}" unfolding sc_def using c1 s(1) s(2) by auto then have *:"flow0 x (s-sc) \ path_image J1" unfolding J1_def path_image_flow_to_path[OF \t1 \ t2\] by blast have "flow0 x (s-sc) = flow0 (flow0 x s) (-sc)" by (smt exist atLeastAtMost_iff existence_ivl_trans' flow_trans s(1) s(2) scd subsetD) then have **:"flow0 (flow0 y (u*t)) (-sc) \ path_image J1" using s(3) * by auto have b:"u*t - sc \ {0.. existence_ivl0 y" using c2 ex by auto then have "flow0 y (u*t - sc) \ path_image J1" using ** by (smt atLeastAtMost_iff diff_existence_ivl_trans ex flow_trans mult_left_le_one_le mult_nonneg_nonneg subset_eq u(1) u(2) yt(2)) thus False using b c3 iemp piJ by blast qed thus "flow0 y (u * t) = flow0 x t1" using s by simp qed thus "\T>0. T \ t \ (\s\{0.. side2) \ flow0 y T \ {flow0 x t1--y t. y \ outer \ 0 \ t \ t \ existence_ivl0 y \ flow0 y t \ closure inner \ \T. 0 < T \ T \ t \ (\s \{0.. outer) \ flow0 y T \ {flow0 x t1--y t. y \ inner \ 0 \ t \ t \ existence_ivl0 y \ flow0 y t \ closure outer \ \T. 0 < T \ T \ t \ (\s \{0.. inner) \ flow0 y T \ {flow0 x t1-- (0::real)" and n: "n = a - b \ n = b - a" and d_ex: "\x. x \ {a -- b} \ {-d..d} \ existence_ivl0 x" and d_above: "\x s. x \ {a -- b} \ 0 < s \ s \ d \ (flow0 x s - x) \ rot n > 0" and d_below: "\x s. x \ {a -- b} \ -d \ s \ s < 0 \ (flow0 x s - x) \ rot n < 0" by blast have ortho: "(a - b) \ rot n = 0" using n by (auto simp: algebra_simps) (* These "rectangles" are either fully inside or fully outside |-----------------------| | r1 | (flow d) a --- (t1) --- rp --- (t2) --- b | r2 | (flow -d) |-----------------------| *) define r1 where "r1 = (\(x, y). flow0 x y)`({flow0 x t1<-- {0<.. {a--b}" by (simp add: open_closed_segment subset_oc_segment x1) then have r1a3: "y \ {flow0 x t1<-- {0<.. existence_ivl0 y" for y using d_ex[of y] by force from flow0_path_connected[OF r1a1 r1a2 r1a3] have pcr1:"path_connected r1" unfolding r1_def by auto have pir1J1: "r1 \ path_image J1 = {}" unfolding J1_def path_image_flow_to_path[OF \t1 \ t2\] proof (rule ccontr) assume "r1 \ flow0 x ` {t1..t2} \ {}" then obtain xx tt ss where eq: "flow0 xx tt = flow0 x ss" and xx: "xx \ {flow0 x t1<-- ss" "ss \ t2" and tt: "0 < tt" "tt < d" unfolding r1_def by force have "xx \ {a -- b}" using sub1b apply (rule set_mp) using xx by (simp add: open_closed_segment) then have [simp]: "xx \ X" using \transversal_segment a b\ by (auto simp: transversal_segment_def) from ss have ss_ex: "ss \ existence_ivl0 x" using exist by auto from d_ex[OF \xx \ {a -- b}\] tt have tt_ex: "tt \ existence_ivl0 xx" by auto then have neg_tt_ex: "- tt \ existence_ivl0 (flow0 xx tt)" by (rule existence_ivl_reverse[simplified]) from eq have "flow0 (flow0 xx tt) (-tt) = flow0 (flow0 x ss) (-tt)" by simp then have "xx = flow0 x (ss - tt)" apply (subst (asm) flow_trans[symmetric]) apply (rule tt_ex) apply (rule neg_tt_ex) apply (subst (asm) flow_trans[symmetric]) apply (rule ss_ex) apply (subst eq[symmetric]) apply (rule neg_tt_ex) by simp moreover define e where "e = ss - t1" consider "e > tt" | "e \ tt" by arith then show False proof cases case 1 have "flow0 (flow0 x ss) (-tt) \ {a<-- {a<-- tt - e" "tt - e \ d" using tt ss 2 e_def by auto have xxtte: "flow0 xx (tt - e) = flow0 x t1" apply (simp add: e_def) by (smt \0 \ tt - e\ \{- d..d} \ existence_ivl0 xx\ atLeastAtMost_iff e_def eq local.existence_ivl_reverse local.existence_ivl_trans local.flow_trans ss(1) ss_ex subset_iff tt(2)) show False proof (cases "tt = e") case True with xxtte have "xx = flow0 x t1" by (simp add: ) with xx show ?thesis apply auto by (auto simp: open_segment_def) next case False with les have "0 < tt - e" by (simp) from d_above[OF \xx \ {a -- b}\ this \tt - e \ d\] have "flow0 xx (tt - e) \ {a -- b}" apply (simp add: in_closed_segment_iff_rot[OF \a \ b\] not_le ) by (smt \xx \ {a--b}\ inner_minus_right inner_rot_neg_move_base inner_rot_pos_move_base n rot_diff_commute) with xxtte show ?thesis using \flow0 x t1 \ {a<-- suba2o by auto qed qed qed (* for sufficiently small d, the flow does not return to the line *) moreover have pir1J2: "r1 \ path_image J2 = {}" proof - have "r1 \ {x. (x - a) \ rot n > 0}" unfolding r1_def proof safe fix aa ba assume "aa \ {flow0 x t1<-- {0<.. rot n" using segment_open_subset_closed[of "flow0 x t1" b] by (intro inner_pos_move_base[OF ortho d_above]) auto qed also have "\ \ {a -- b} = {}" using in_segment_inner_rot in_segment_inner_rot2 n by auto finally show ?thesis unfolding J2_def path_image_linepath using t12sub open_closed_segment by (force simp: closed_segment_commute) qed ultimately have pir1:"r1 \ (path_image J) = {}" unfolding J_def by (metis disjoint_iff_not_equal not_in_path_image_join) define r2 where "r2 =(\(x, y). flow0 x y)`({a <--< flow0 x t2} \ {-d<..<0})" have r2a1:"path_connected {a <--< flow0 x t2}" by simp have r2a2:"path_connected {-d<..<0}" by simp have "{a <--< flow0 x t2} \ {a -- b}" by (meson ends_in_segment(1) open_closed_segment subset_co_segment subset_oc_segment t12sub) then have r2a3: "y \ {a <--< flow0 x t2} \ {-d<..<0} \ existence_ivl0 y" for y using d_ex[of y] by force from flow0_path_connected[OF r2a1 r2a2 r2a3] have pcr2:"path_connected r2" unfolding r2_def by auto have pir2J2: "r2 \ path_image J1 = {}" unfolding J1_def path_image_flow_to_path[OF \t1 \ t2\] proof (rule ccontr) assume "r2 \ flow0 x ` {t1..t2} \ {}" then obtain xx tt ss where eq: "flow0 xx tt = flow0 x ss" and xx: "xx \ {a<-- ss" "ss \ t2" and tt: "-d < tt" "tt < 0" unfolding r2_def by force have "xx \ {a -- b}" using suba2 apply (rule set_mp) using xx by (simp add: open_closed_segment) then have [simp]: "xx \ X" using \transversal_segment a b\ by (auto simp: transversal_segment_def) from ss have ss_ex: "ss \ existence_ivl0 x" using exist by auto from d_ex[OF \xx \ {a -- b}\] tt have tt_ex: "tt \ existence_ivl0 xx" by auto then have neg_tt_ex: "- tt \ existence_ivl0 (flow0 xx tt)" by (rule existence_ivl_reverse[simplified]) from eq have "flow0 (flow0 xx tt) (-tt) = flow0 (flow0 x ss) (-tt)" by simp then have "xx = flow0 x (ss - tt)" apply (subst (asm) flow_trans[symmetric]) apply (rule tt_ex) apply (rule neg_tt_ex) apply (subst (asm) flow_trans[symmetric]) apply (rule ss_ex) apply (subst eq[symmetric]) apply (rule neg_tt_ex) by simp moreover define e where "e = t2 - ss" consider "e > - tt" | "e \ -tt" by arith then show False proof cases case 1 have "flow0 (flow0 x ss) (-tt) \ {a<-- {a<-- 0" "-d \ tt + e" using tt ss 2 e_def by auto have xxtte: "flow0 xx (tt + e) = flow0 x t2" apply (simp add: e_def) by (smt atLeastAtMost_iff calculation eq exist local.existence_ivl_trans' local.flow_trans neg_tt_ex ss_ex subset_iff \t1 \ t2\) show False proof (cases "tt=-e") case True with xxtte have "xx = flow0 x t2" by (simp add: ) with xx show ?thesis apply auto by (auto simp: open_segment_def) next case False with les have "tt+e < 0" by simp from d_below[OF \xx \ {a -- b}\ \-d \ tt + e\ this] have "flow0 xx (tt + e) \ {a -- b}" apply (simp add: in_closed_segment_iff_rot[OF \a \ b\] not_le ) by (smt \xx \ {a--b}\ inner_minus_right inner_rot_neg_move_base inner_rot_pos_move_base n rot_diff_commute) with xxtte show ?thesis using \flow0 x t2 \ {a--b}\ by simp qed qed qed moreover have pir2J2: "r2 \ path_image J2 = {}" proof - have "r2 \ {x. (x - a) \ rot n < 0}" unfolding r2_def proof safe fix aa ba assume "aa \ {a<-- {-d<..<0}" with suba2 show "0 > (flow0 aa ba - a) \ rot n" using segment_open_subset_closed[of a "flow0 x t2"] by (intro inner_neg_move_base[OF ortho d_below]) auto qed also have "\ \ {a -- b} = {}" using in_segment_inner_rot in_segment_inner_rot2 n by auto finally show ?thesis unfolding J2_def path_image_linepath using t12sub open_closed_segment by (force simp: closed_segment_commute) qed ultimately have pir2:"r2 \ (path_image J) = {}" unfolding J_def by (metis disjoint_iff_not_equal not_in_path_image_join) define rp where "rp = midpoint (flow0 x t1) (flow0 x t2)" have rpi: "rp \ {flow0 x t1<-- {a -- b}" using rpi suba2o subl by blast then have [simp]: "rp \ X" using \{a--b} \ X\ by blast (* The fundamental case distinction *) have *: "pathfinish J1 = flow0 x t2" "pathstart J1 = flow0 x t1" "rp \ {flow0 x t2<-- rot (flow0 x t2 - flow0 x t1)} = {y. 0 < (y - rp) \ rot (flow0 x t2 - flow0 x t1)}" by (smt Collect_cong in_open_segment_rotD inner_diff_left nrm_dot rpi) also have "... = {y. 0 > (y - rp) \ rot (flow0 x t1 - flow0 x t2)}" by (smt Collect_cong inner_minus_left nrm_reverse) also have " ... = {y. 0 > (y - rp) \ rot (a - b) }" by (metis rot_same_dir(2) x1 x2) finally have side1: "{y. 0 < (y - flow0 x t2) \ rot (flow0 x t2 - flow0 x t1)} = {y. 0 > (y - rp) \ rot (a - b) }" (is "_ = ?lower1") . have "{y. (y - flow0 x t2) \ rot (flow0 x t2 - flow0 x t1) < 0} = {y. (y - rp) \ rot (flow0 x t2 - flow0 x t1) < 0}" by (smt Collect_cong in_open_segment_rotD inner_diff_left nrm_dot rpi) also have "... = {y. (y - rp) \ rot (flow0 x t1 - flow0 x t2) > 0}" by (smt Collect_cong inner_minus_left nrm_reverse) also have " ... = {y. 0 < (y - rp) \ rot (a - b) }" by (metis rot_same_dir(1) x1 x2) finally have side2: "{y. (y - flow0 x t2) \ rot (flow0 x t2 - flow0 x t1) < 0} = {y. 0 < (y - rp) \ rot (a - b) }" (is "_ = ?upper1") . from linepath_ball_inside_outside[OF \simple_path J\[unfolded J_def J2_def] *, folded J2_def J_def, unfolded side1 side2] obtain e where e0: "0 < e" "ball rp e \ path_image J1 = {}" "ball rp e \ ?lower1 \ inner \ ball rp e \ ?upper1 \ outer \ ball rp e \ ?upper1 \ inner \ ball rp e \ ?lower1 \ outer" by (auto simp: inner_def outer_def) let ?lower = "{y. 0 > (y - rp) \ rot n }" let ?upper = "{y. 0 < (y - rp) \ rot n }" have "?lower1 = {y. 0 < (y - rp) \ rot n } \ ?upper1 = {y. 0 > (y - rp) \ rot n } \ ?lower1 = {y. 0 > (y - rp) \ rot n } \ ?upper1 = {y. 0 < (y - rp) \ rot n }" using n rot_diff_commute[of a b] by auto from this e0 have e: "0 < e" "ball rp e \ path_image J1 = {}" "ball rp e \ ?lower \ inner \ ball rp e \ ?upper \ outer \ ball rp e \ ?upper \ inner \ ball rp e \ ?lower \ outer" by auto have "\\<^sub>F t in at_right 0. t < d" by (auto intro!: order_tendstoD \0 < d\) then have evr: "\\<^sub>F t in at_right 0. 0 < (flow0 rp t - rp) \ rot n" unfolding eventually_at_filter by eventually_elim (auto intro!: \rp \ {a--b}\ d_above) have "\\<^sub>F t in at_left 0. t > -d" by (auto intro!: order_tendstoD \0 < d\) then have evl: "\\<^sub>F t in at_left 0. 0 > (flow0 rp t - rp) \ rot n" unfolding eventually_at_filter by eventually_elim (auto intro!: \rp \ {a--b}\ d_below) have "\\<^sub>F t in at 0. flow0 rp t \ ball rp e" unfolding mem_ball apply (subst dist_commute) apply (rule tendstoD) by (auto intro!: tendsto_eq_intros \0 < e\) then have evl2: "(\\<^sub>F t in at_left 0. flow0 rp t \ ball rp e)" and evr2: "(\\<^sub>F t in at_right 0. flow0 rp t \ ball rp e)" unfolding eventually_at_split by auto have evl3: "(\\<^sub>F t in at_left 0. t > -d)" and evr3: "(\\<^sub>F t in at_right 0. t < d)" by (auto intro!: order_tendstoD \0 < d\) have evl4: "(\\<^sub>F t in at_left 0. t < 0)" and evr4: "(\\<^sub>F t in at_right 0. t > 0)" by (auto simp: eventually_at_filter) from evl evl2 evl3 evl4 have "\\<^sub>F t in at_left 0. (flow0 rp t - rp) \ rot n < 0 \ flow0 rp t \ ball rp e \ t > -d \ t < 0" by eventually_elim auto from eventually_happens[OF this] obtain dl where dl: "(flow0 rp dl - rp) \ rot n < 0" "flow0 rp dl \ ball rp e" "- d < dl" "dl < 0" by auto from evr evr2 evr3 evr4 have "\\<^sub>F t in at_right 0. (flow0 rp t - rp) \ rot n > 0 \ flow0 rp t \ ball rp e \ t < d \ t > 0" by eventually_elim auto from eventually_happens[OF this] obtain dr where dr: "(flow0 rp dr - rp) \ rot n > 0" "flow0 rp dr \ ball rp e" "d > dr" "dr > 0" by auto have "rp \ {flow0 x t1<-- r1" unfolding r1_def using \d > dr\ \dr > 0\ by auto have "rp \ {a<-- r2" unfolding r2_def using \-d < dl\ \dl < 0\ by auto from e(3) dr dl have "flow0 rp (dr) \ outer \ flow0 rp (dl) \ inner \ flow0 rp (dr) \ inner \ flow0 rp (dl) \ outer" by auto moreover { assume "flow0 rp dr \ outer" "flow0 rp dl \ inner" then have r1o: "r1 \ outer \ {}" and r2i: "r2 \ inner \ {}" using rpr1 rpr2 by auto from path_connected_not_frontier_subset[OF pcr1 r1o] have "r1 \ outer" using pir1 by (simp add: io(12)) from path_connected_not_frontier_subset[OF pcr2 r2i] have "r2 \ inner" using pir2 by (simp add: io(11)) have "(\(x, y). flow0 x y)`({flow0 x t2} \ {0<.. r1" unfolding r1_def by (auto intro!:image_mono simp add: x2) then have *:"\t. 0 < t \ t < d \ flow0 (flow0 x t2) t \ outer" by (smt \r1 \ outer\ greaterThanLessThan_iff mem_Sigma_iff pair_imageI r1_def subset_eq x2) then have t2o: "\t. 0 < t \ t < d \ flow0 x (t2 + t) \ outer" using r1a3[OF x2] exist flow_trans by (metis (no_types, hide_lams) closed_segment_commute ends_in_segment(1) local.existence_ivl_trans' local.flow_undefined0 real_Icc_closed_segment subset_eq \t1 \ t2\) (* Construct a sequence of times converging to these points in r2 \ inner *) have inner: "{a <--< flow0 x t2} \ closure inner" proof (rule subsetI) fix y assume y: "y \ {a <--< flow0 x t2}" have [simp]: "y \ X" using y suba12_open suba2o \{a -- b} \ X\ by auto have "(\n. flow0 y (- d / real (Suc (Suc n))) \ inner)" using y using suba12_open \0 < d\ suba2o \{a -- b} \ X\ by (auto intro!: set_mp[OF \r2 \ inner\] image_eqI[where x="(y, -d/Suc (Suc n))" for n] simp: r2_def divide_simps) moreover have d_over_0: "(\s. - d / real (Suc (Suc s))) \ 0" by (rule real_tendsto_divide_at_top) (auto intro!: filterlim_tendsto_add_at_top filterlim_real_sequentially) have "(\n. flow0 y (- d / real (Suc (Suc n)))) \ y" apply (rule tendsto_eq_intros) apply (rule tendsto_intros) apply (rule d_over_0) by auto ultimately show "y \ closure inner" unfolding closure_sequential by (intro exI[where x="\n. flow0 y (-d/Suc (Suc n))"]) (rule conjI) qed then have "{a <--< flow0 x t1} \ closure inner" using suba12_open by blast then have "{flow0 x t1 -- flow0 x t2} \ closure inner" by (metis (no_types, lifting) closure_closure closure_mono closure_open_segment dual_order.trans inner subl x1neqx2) have outer:"\t. t > t2 \ t \ existence_ivl0 x \ flow0 x t \ outer" proof (rule ccontr) fix t assume t: "t > t2" "t \ existence_ivl0 x" "flow0 x t \ outer" have "0 \ t- (t2+d)" using t2o t by smt then have a2:"0 \ t - (t2+dr)" using d \0 < dr\ \dr < d\ by linarith have t2d2_ex: "t2 + dr \ existence_ivl0 x" using \t1 \ t2\ exist d_ex[of "flow0 x t2"] \flow0 x t2 \ {a--b}\ \0 < d\ \0 < dr\ \dr < d\ by (intro existence_ivl_trans) auto then have a3: "t - (t2 + dr) \ existence_ivl0 (flow0 x (t2 + dr))" using t(2) by (intro diff_existence_ivl_trans) auto then have "flow0 (flow0 x (t2 + dr)) (t - (t2 + dr)) = flow0 x t" by (subst flow_trans[symmetric]) (auto simp: t2d2_ex) moreover have "flow0 x t \ closure inner" using t(3) io by (metis ComplI Un_iff closure_Un_frontier) ultimately have a4: "flow0 (flow0 x (t2 + dr)) (t - (t2 + dr)) \ closure inner" by auto have a1: "flow0 x (t2+dr) \ outer" by (simp add: d t2o \0 < dr\ \dr < d\) from outside_in[OF a1 a2 a3 a4] obtain T where T: "T > 0" "T \ t - (t2 + dr)" "(\s\{0.. outer)" "flow0 (flow0 x (t2 + dr)) T \ {flow0 x t1 --< flow0 x t2}" by blast define y where "y = flow0 (flow0 x (t2 + dr)) T" have "y \ {a <--< flow0 x t2}" unfolding y_def using T(4) using subl2 by blast then have "(\(x, y). flow0 x y)`({y} \ {-d<..<0}) \ r2" unfolding r2_def by (auto intro!:image_mono) then have *:"\t. -d < t \ t < 0 \ flow0 y t \ r2" by (simp add: pair_imageI subsetD) have "max (-T/2) dl < 0" using d T \0 > dl\ \dl > -d\ by auto moreover have "-d < max (-T/2) dl" using d T \0 > dl\ \dl > -d\ by auto ultimately have inner: "flow0 y (max (-T/2) dl) \ inner" using * \r2 \ inner\ by blast have "0\(T+(max (-T/2) dl))" using T(1) by linarith moreover have "(T+(max (-T/2) dl)) < T" using T(1) d \0 > dl\ \dl > -d\ by linarith ultimately have outer: " flow0 (flow0 x (t2 + dr)) (T+(max (-T/2) dl)) \ outer" using T by auto have T_ex: "T \ existence_ivl0 (flow0 x (t2 + dr))" apply (subst flow_trans) using exist \t1 \ t2\ using d_ex[of "flow0 x t2"] \flow0 x t2 \ {a -- b}\ \d > 0\ T \0 < dr\ \dr < d\ apply (auto simp: ) apply (rule set_rev_mp[where A="{0 .. t - (t2 + dr)}"], force) apply (rule ivl_subset_existence_ivl) apply (rule existence_ivl_trans') apply (rule existence_ivl_trans') by (auto simp: t) have T_ex2: "dr + T \ existence_ivl0 (flow0 x t2)" by (smt T_ex ends_in_segment(2) exist local.existence_ivl_trans local.existence_ivl_trans' real_Icc_closed_segment subset_eq t2d2_ex \t1 \ t2\) thus False using T \t1 \ t2\ exist by (smt T_ex diff_existence_ivl_trans disjoint_iff_not_equal inner io(9) local.flow_trans local.flow_undefined0 outer y_def) qed have "closure inner \ outer = {}" by (simp add: inf_sup_aci(1) io(5) io(9) open_Int_closure_eq_empty) then have "flow0 x t \ {a<--t > t2\ \t \ existence_ivl0 x\ inner outer by blast } moreover { assume "flow0 rp dr \ inner" "flow0 rp dl \ outer" then have r1i: "r1 \ inner \ {}" and r2o: "r2 \ outer \ {}" using rpr1 rpr2 by auto from path_connected_not_frontier_subset[OF pcr1 r1i] have "r1 \ inner" using pir1 by (simp add: io(11)) from path_connected_not_frontier_subset[OF pcr2 r2o] have "r2 \ outer" using pir2 by (simp add: io(12)) have "(\(x, y). flow0 x y)`({flow0 x t2} \ {0<.. r1" unfolding r1_def by (auto intro!:image_mono simp add: x2) then have *:"\t. 0 < t \ t < d \ flow0 (flow0 x t2) t \ inner" by (smt \r1 \ inner\ greaterThanLessThan_iff mem_Sigma_iff pair_imageI r1_def subset_eq x2) then have t2o: "\t. 0 < t \ t < d \ flow0 x (t2 + t) \ inner" using r1a3[OF x2] exist flow_trans by (metis (no_types, hide_lams) closed_segment_commute ends_in_segment(1) local.existence_ivl_trans' local.flow_undefined0 real_Icc_closed_segment subset_eq \t1 \ t2\) (* Construct a sequence of times converging to these points in r2 \ outer *) have outer: "{a <--< flow0 x t2} \ closure outer" proof (rule subsetI) fix y assume y: "y \ {a <--< flow0 x t2}" have [simp]: "y \ X" using y suba12_open suba2o \{a -- b} \ X\ by auto have "(\n. flow0 y (- d / real (Suc (Suc n))) \ outer)" using y using suba12_open \0 < d\ suba2o \{a -- b} \ X\ by (auto intro!: set_mp[OF \r2 \ outer\] image_eqI[where x="(y, -d/Suc (Suc n))" for n] simp: r2_def divide_simps) moreover have d_over_0: "(\s. - d / real (Suc (Suc s))) \ 0" by (rule real_tendsto_divide_at_top) (auto intro!: filterlim_tendsto_add_at_top filterlim_real_sequentially) have "(\n. flow0 y (- d / real (Suc (Suc n)))) \ y" apply (rule tendsto_eq_intros) apply (rule tendsto_intros) apply (rule d_over_0) by auto ultimately show "y \ closure outer" unfolding closure_sequential by (intro exI[where x="\n. flow0 y (-d/Suc (Suc n))"]) (rule conjI) qed then have "{a <--< flow0 x t1} \ closure outer" using suba12_open by blast then have "{flow0 x t1 -- flow0 x t2} \ closure outer" by (metis (no_types, lifting) closure_closure closure_mono closure_open_segment dual_order.trans outer subl x1neqx2) have inner:"\t. t > t2 \ t \ existence_ivl0 x \ flow0 x t \ inner" proof (rule ccontr) fix t assume t: "t > t2" "t \ existence_ivl0 x" "flow0 x t \ inner" have "0 \ t- (t2+d)" using t2o t by smt then have a2:"0 \ t - (t2+dr)" using d \0 < dr\ \dr < d\ by linarith have t2d2_ex: "t2 + dr \ existence_ivl0 x" using \t1 \ t2\ exist d_ex[of "flow0 x t2"] \flow0 x t2 \ {a--b}\ \0 < d\ \0 < dr\ \dr < d\ by (intro existence_ivl_trans) auto then have a3: "t - (t2 + dr) \ existence_ivl0 (flow0 x (t2 + dr))" using t(2) by (intro diff_existence_ivl_trans) auto then have "flow0 (flow0 x (t2 + dr)) (t - (t2 + dr)) = flow0 x t" by (subst flow_trans[symmetric]) (auto simp: t2d2_ex) moreover have "flow0 x t \ closure outer" using t(3) io by (metis ComplI Un_iff closure_Un_frontier) ultimately have a4: "flow0 (flow0 x (t2 + dr)) (t - (t2 + dr)) \ closure outer" by auto have a1: "flow0 x (t2+dr) \ inner" by (simp add: d t2o \0 < dr\ \dr < d\) from inside_out[OF a1 a2 a3 a4] obtain T where T: "T > 0" "T \ t - (t2 + dr)" "(\s\{0.. inner)" "flow0 (flow0 x (t2 + dr)) T \ {flow0 x t1 --< flow0 x t2}" by blast define y where "y = flow0 (flow0 x (t2 + dr)) T" have "y \ {a <--< flow0 x t2}" unfolding y_def using T(4) using subl2 by blast then have "(\(x, y). flow0 x y)`({y} \ {-d<..<0}) \ r2" unfolding r2_def by (auto intro!:image_mono) then have *:"\t. -d < t \ t < 0 \ flow0 y t \ r2" by (simp add: pair_imageI subsetD) have "max (-T/2) dl < 0" using d T \0 > dl\ \dl > -d\ by auto moreover have "-d < max (-T/2) dl" using d T \0 > dl\ \dl > -d\ by auto ultimately have outer: "flow0 y (max (-T/2) dl) \ outer" using * \r2 \ outer\ by blast have "0\(T+(max (-T/2) dl))" using T(1) by linarith moreover have "(T+(max (-T/2) dl)) < T" using T(1) d \0 > dl\ \dl > -d\ by linarith ultimately have inner: " flow0 (flow0 x (t2 + dr)) (T+(max (-T/2) dl)) \ inner" using T by auto have T_ex: "T \ existence_ivl0 (flow0 x (t2 + dr))" apply (subst flow_trans) using exist \t1 \ t2\ using d_ex[of "flow0 x t2"] \flow0 x t2 \ {a -- b}\ \d > 0\ T \0 < dr\ \dr < d\ apply (auto simp: ) apply (rule set_rev_mp[where A="{0 .. t - (t2 + dr)}"], force) apply (rule ivl_subset_existence_ivl) apply (rule existence_ivl_trans') apply (rule existence_ivl_trans') by (auto simp: t) have T_ex2: "dr + T \ existence_ivl0 (flow0 x t2)" by (smt T_ex ends_in_segment(2) exist local.existence_ivl_trans local.existence_ivl_trans' real_Icc_closed_segment subset_eq t2d2_ex \t1 \ t2\) thus False using T \t1 \ t2\ exist by (smt T_ex diff_existence_ivl_trans disjoint_iff_not_equal inner io(9) local.flow_trans local.flow_undefined0 outer y_def) qed have "closure outer \ inner = {}" by (metis inf_sup_aci(1) io(2) io2(1) open_Int_closure_eq_empty) then have "flow0 x t \ {a<--t > t2\ \t \ existence_ivl0 x\ inner outer by blast } ultimately show "flow0 x t \ {a<-- {a<-- {a<-- y \ {x<-- y \ {a<-- {y} \ {y<-- {a<-- x = y \ x \ {y <-- {a<-- {x<-- {y<-- {a<-- t2" assumes "{t1..t2} \ existence_ivl0 x" assumes x1: "flow0 x t1 \ {a<-- {a<--t. t \ {t1<.. flow0 x t \ {a<-- existence_ivl0 x" shows "flow0 x t \ {a<--{t1..t2} \ existence_ivl0 x\ note t1t2 = \\t. t \ {t1<.. flow0 x t \ {a<-- from \transversal_segment a b\ have [simp]: "a \ b" by (simp add: transversal_segment_def) from x1 obtain i1 where i1: "flow0 x t1 = line a b i1" "0 < i1" "i1 < 1" by (auto simp: in_open_segment_iff_line) from x2 obtain i2 where i2: "flow0 x t2 = line a b i2" "0 < i2" "i2 < i1" by (auto simp: i1 open_segment_line_iff) have t2_exist[simp]: "t2 \ existence_ivl0 x" using \t1 \ t2\ exist by auto have t2_mem: "flow0 x t2 \ {a<-- {flow0 x t2<--transversal_segment a b\ unfolding rev_transversal_segment . have time': "0 \ t2 - t1" using \t1 \ t2\ by simp have [simp, intro]: "flow0 x t2 \ X" using exist \t1 \ t2\ by auto have exivl': "{0..t2 - t1} \ rev.existence_ivl0 (flow0 x t2)" using exist \t1 \ t2\ by (force simp add: rev_existence_ivl_eq0 intro!: existence_ivl_trans') have step': "rev.flow0 (flow0 x t2) (t2-t) \ {a<--t1 \ t2\ x1 x2 t2_mem x1_mem t1t2 \t < t1\ \t \ existence_ivl0 x\ apply (auto simp: rev_existence_ivl_eq0 rev_eq_flow existence_ivl_trans' flow_trans[symmetric]) by (subst (asm) flow_trans[symmetric]) (auto intro!: existence_ivl_trans') then show ?thesis unfolding rev_eq_flow using \t1 \ t2\ exist \t < t1\ \t \ existence_ivl0 x\ by (auto simp: flow_trans[symmetric] existence_ivl_trans') qed lemma flow0_transversal_segment_monotone_step_reverse2: assumes transversal: "transversal_segment a b" assumes time: "t1 \ t2" assumes exist: "{t1..t2} \ existence_ivl0 x" assumes t1: "flow0 x t1 \ {a<-- {flow0 x t1<--t. t \ {t1<.. flow0 x t \ {a<-- existence_ivl0 x" shows "flow0 x t \ {flow0 x t1<-- t2" assumes exist: "{t1..t2} \ existence_ivl0 x" assumes t1: "flow0 x t1 \ {a<-- {a<--t. t \ {t1<.. flow0 x t \ {a<--t. t > t2 \ t \ existence_ivl0 x \ flow0 x t \ {flow0 x t2<-- t2" assumes "{t1..t2} \ existence_ivl0 x" assumes x1: "flow0 x t1 \ {a<-- {flow0 x t1<-- t2" "t \ existence_ivl0 x" shows "flow0 x t \ {a<--{t1..t2} \ existence_ivl0 x\ note t = \t > t2\ \t \ existence_ivl0 x\ have x1neqx2: "flow0 x t1 \ flow0 x t2" using open_segment_def x2 by force then have t1neqt2: "t1 \ t2" by auto with \t1 \ t2\ have "t1 < t2" by simp from \transversal_segment a b\ have [simp]: "a \ b" by (simp add: transversal_segment_def) from x1 obtain i1 where i1: "flow0 x t1 = line a b i1" "0 < i1" "i1 < 1" by (auto simp: in_open_segment_iff_line) from x2 i1 obtain i2 where i2: "flow0 x t2 = line a b i2" "i1 < i2" "i2 < 1" by (auto simp: line_open_segment_iff) have t2_in: "flow0 x t2 \ {a<--transversal_segment a b\ \t1 \ t2\ exist] have "finite ?T" . then have "finite ?T'" by (rule finite_subset[rotated]) (auto simp: open_closed_segment) have "?T' \ {}" by (auto intro!: exI[where x=t1] \t1 < t2\ x1) note tm_defined = \finite ?T'\ \?T' \ {}\ define tm where "tm = Max ?T'" have "tm \ ?T'" unfolding tm_def using tm_defined by (rule Max_in) have tm_in: "flow0 x tm \ {a<--tm \ ?T'\ by auto have tm: "t1 \ tm" "tm < t2" "tm \ t2" using \tm \ ?T'\ by auto have tm_Max: "t \ tm" if "t \ ?T'" for t unfolding tm_def using tm_defined(1) that by (rule Max_ge) have tm_exclude: "flow0 x t \ {a<-- {tm<..tm \ ?T'\ tm_Max that by auto (meson approximation_preproc_push_neg(2) dual_order.strict_trans2 le_cases) have "{tm..t2} \ existence_ivl0 x" using exist tm by auto from open_segment_trichotomy[OF tm_in t2_in] consider "flow0 x t2 \ {flow0 x tm<-- {a<-- {a<--transversal_segment a b\ \tm \ t2\ \{tm..t2} \ existence_ivl0 x\ tm_in 1 tm_exclude t] show ?thesis . next case 2 have "t1 \ tm" using 2 x2 i1 i2 by (auto simp: line_in_subsegment line_in_subsegment2) then have "t1 < tm" using \t1 \ tm\ by simp from flow0_transversal_segment_monotone_step_reverse[OF \transversal_segment a b\ \tm \ t2\ \{tm..t2} \ existence_ivl0 x\ tm_in 2 tm_exclude \t1 < tm\] exist \t1 \ t2\ have "flow0 x t1 \ {a<-- tm" using 3 x2 by (auto simp: open_segment_def) then have "t1 < tm" using \t1 \ tm\ by simp have "range (flow0 x) = flow0 x ` {tm..t2}" apply (rule recurrence_time_restricts_compact_flow'[OF \tm < t2\ _ _ 3]) using exist \t1 \ t2\ \t1 < tm\ \tm < t2\ by auto also have "\ = flow0 x ` (insert t2 {tm<..tm \ t2\ 3 apply (auto simp: ) by (smt greaterThanLessThan_iff image_eqI) finally have "flow0 x t1 \ flow0 x ` (insert t2 {tm<.. flow0 x ` {tm<.. \ {a<--Straightening\ text \ This lemma uses the implicit function theorem \ lemma cross_time_continuous: assumes "transversal_segment a b" assumes "x \ {a<-- 0" obtains d t where "d > 0" "continuous_on (ball x d) t" "\y. y \ ball x d \ flow0 y (t y) \ {a<--y. y \ ball x d \ \t y\ < e" "continuous_on (ball x d) t" "t x = 0" proof - have "x \ X" using assms segment_open_subset_closed[of a b] by (auto simp: transversal_segment_def) have "a \ b" using assms by auto define s where "s x = (x - a) \ rot (b - a)" for x have "s x = 0" unfolding s_def by (subst in_segment_inner_rot) (auto intro!: assms open_closed_segment) have Ds: "(s has_derivative blinfun_inner_left (rot (b - a))) (at x)" (is "(_ has_derivative blinfun_apply (?Ds x)) _") for x unfolding s_def by (auto intro!: derivative_eq_intros) have Dsc: "isCont ?Ds x" by (auto intro!: continuous_intros) have nz: "?Ds x (f x) \ 0" using assms apply auto unfolding transversal_segment_def by (smt inner_minus_left nrm_reverse open_closed_segment) from flow_implicit_function_at[OF \x \ X\, of s, OF \s x = 0\ Ds Dsc nz \e > 0\] obtain t d1 where "0 < d1" and t0: "t x = 0" and d1: "(\y. y \ cball x d1 \ s (flow0 y (t y)) = 0)" "(\y. y \ cball x d1 \ \t y\ < e)" "(\y. y \ cball x d1 \ t y \ existence_ivl0 y)" and tc: "continuous_on (cball x d1) t" and t': "(t has_derivative (- blinfun_inner_left (rot (b - a)) /\<^sub>R (blinfun_inner_left (rot (b - a))) (f x))) (at x)" by metis from tc have "t \x\ 0" using \0 < d1\ by (auto simp: continuous_on_def at_within_interior t0 dest!: bspec[where x=x]) then have ftc: "((\y. flow0 y (t y)) \ x) (at x)" by (auto intro!: tendsto_eq_intros simp: \x \ X\) define e2 where "e2 = min (dist a x) (dist b x)" have "e2 > 0" using assms by (auto simp: e2_def open_segment_def) from tendstoD[OF ftc this] have "\\<^sub>F y in at x. dist (flow0 y (t y)) x < e2" . moreover let ?S = "{x. a \ (b - a) < x \ (b - a) \ x \ (b - a) < b \ (b - a)}" have "open ?S" "x \ ?S" using \x \ {a<-- by (auto simp add: open_segment_line_hyperplanes \a \ b\ intro!: open_Collect_conj open_halfspace_component_gt open_halfspace_component_lt) from topological_tendstoD[OF ftc this] have "\\<^sub>F y in at x. flow0 y (t y) \ ?S" . ultimately have "\\<^sub>F y in at x. flow0 y (t y) \ ball x e2 \ ?S" by eventually_elim (auto simp: dist_commute) then obtain d2 where "0 < d2" and "\y. x \ y \ dist y x < d2 \ flow0 y (t y) \ ball x e2 \ ?S" by (force simp: eventually_at) then have d2: "dist y x < d2 \ flow0 y (t y) \ ball x e2 \ ?S" for y using \0 < e2\ \x \ X\ t0 \x \ ?S\ by (cases "y = x") auto define d where "d = min d1 d2" have "d > 0" using \0 < d1\ \0 < d2\ by (simp add: d_def) moreover have "continuous_on (ball x d) t" by (auto intro!:continuous_on_subset[OF tc] simp add: d_def) moreover have "ball x e2 \ ?S \ {x. s x = 0} \ {a<--a \ b\) (auto simp: s_def e2_def in_segment) then have "\y. y \ ball x d \ flow0 y (t y) \ {a<--0 < d2\ by (auto simp: d_def e2_def dist_commute) moreover have "\y. y \ ball x d \ \t y\ < e" using d1 by (auto simp: d_def) moreover have "continuous_on (ball x d) t" using tc by (rule continuous_on_subset) (auto simp: d_def) moreover have "t x = 0" by (simp add: t0) ultimately show ?thesis .. qed lemma \_limit_crossings: assumes "transversal_segment a b" assumes pos_ex: "{0..} \ existence_ivl0 x" assumes "\_limit_point x p" assumes "p \ {a<--\<^bsub>\<^esub> \" "(flow0 x \ s) \ p" "\\<^sub>F n in sequentially. flow0 x (s n) \ {a<-- s n \ existence_ivl0 x" proof - from assms have "p \ X" by (auto simp: transversal_segment_def open_closed_segment) from assms(3) obtain t where "t \\<^bsub>\<^esub> \" "(flow0 x \ t) \ p" by (auto simp: \_limit_point_def) note t = \t \\<^bsub>\<^esub> \\ \(flow0 x \ t) \ p\ note [tendsto_intros] = t(2) from cross_time_continuous[OF assms(1,4) zero_less_one\ \TODO ??\] obtain \ \ where "0 < \" "continuous_on (ball p \) \" "\ p = 0" "(\y. y \ ball p \ \ \\ y\ < 1)" "(\y. y \ ball p \ \ flow0 y (\ y) \ {a<-- = \(\y. y \ ball p \ \ flow0 y (\ y) \ {a<-- \(\y. y \ ball p \ \ \\ y\ < 1)\ \continuous_on (ball p \) \\ \\ p = 0\ define s where "s n = t n + \ (flow0 x (t n))" for n have ev_in_ball: "\\<^sub>F n in at_top. flow0 x (t n) \ ball p \" apply (simp add: ) apply (subst dist_commute) apply (rule tendstoD) apply (rule t[unfolded o_def]) apply (rule \0 < \\) done have "filterlim s at_top sequentially" proof (rule filterlim_at_top_mono) show "filterlim (\n. -1 + t n) at_top sequentially" by (rule filterlim_tendsto_add_at_top) (auto intro!: filterlim_tendsto_add_at_top t) from ev_in_ball show "\\<^sub>F x in sequentially. -1 + t x \ s x" apply eventually_elim using \ by (force simp : s_def) qed moreover have \_cont: "\ \p\ \ p" using \(3) \0 < \\ by (auto simp: continuous_on_def at_within_ball dest!: bspec[where x=p]) note [tendsto_intros] = tendsto_compose_at[OF _ this, simplified] have ev1: "\\<^sub>F n in sequentially. t n > 1" using filterlim_at_top_dense t(1) by auto then have ev_eq: "\\<^sub>F n in sequentially. flow0 ((flow0 x o t) n) ((\ o (flow0 x o t)) n) = (flow0 x o s) n" using ev_in_ball apply (eventually_elim) apply (drule \(2)) unfolding o_def apply (subst flow_trans[symmetric]) using pos_ex apply (auto simp: s_def) apply (rule existence_ivl_trans') by auto then have "\\<^sub>F n in sequentially. (flow0 x o s) n = flow0 ((flow0 x o t) n) ((\ o (flow0 x o t)) n)" by (simp add: eventually_mono) from \(flow0 x \ t) \ p\ and \\ \p\ \ p\ have "(\n. flow0 ((flow0 x \ t) n) ((\ \ (flow0 x \ t)) n)) \ flow0 p (\ p)" using \\ p = 0\ \_cont \p \ X\ by (intro tendsto_eq_intros) auto - with ev_eq have "(flow0 x o s) \ flow0 p (\ p)" - by (rule Lim_transform_eventually) + then have "(flow0 x o s) \ flow0 p (\ p)" + using ev_eq by (rule Lim_transform_eventually) then have "(flow0 x o s) \ p" using \p \ X\ \\ p = 0\ by simp moreover { have "\\<^sub>F n in sequentially. flow0 x (s n) \ {a<--) by simp moreover have "\\<^sub>F n in sequentially. s n \ existence_ivl0 x" using ev_in_ball ev1 apply (eventually_elim) apply (drule \(2)) using pos_ex by (auto simp: s_def) ultimately have "\\<^sub>F n in sequentially. flow0 x (s n) \ {a<-- s n \ existence_ivl0 x" by eventually_elim auto } ultimately show ?thesis .. qed (* Obvious but frequently used step *) lemma filterlim_at_top_tendstoE: assumes "e > 0" assumes "filterlim s at_top sequentially" assumes "(flow0 x \ s) \ u" assumes "\\<^sub>F n in sequentially. P (s n)" obtains m where "m > b" "P m" "dist (flow0 x m) u < e" proof - from assms(2) have "\\<^sub>F n in sequentially. b < s n" by (simp add: filterlim_at_top_dense) moreover have "\\<^sub>F n in sequentially. norm ((flow0 x \ s) n - u) < e" using assms(3)[THEN tendstoD, OF assms(1)] by (simp add: dist_norm) moreover note assms(4) ultimately have "\\<^sub>F n in sequentially. b < s n \ norm ((flow0 x \ s) n - u) < e \ P (s n)" by eventually_elim auto then obtain m where "m > b" "P m" "dist (flow0 x m) u < e" by (auto simp add: eventually_sequentially dist_norm) then show ?thesis .. qed lemma open_segment_separate_left: fixes u v x a b::'a assumes u:"u \ {a <--< b}" assumes v:"v \ {u <--< b}" assumes x: "dist x u < dist u v" "x \ {a <--< b}" shows "x \ {a <--< v}" proof - have "v \ x" by (smt dist_commute x(1)) moreover have "x \ {v<-- {a<-- {a <--< b}" assumes v:"v \ {a <--< u}" assumes x: "dist x u < dist u v" "x \ {a <--< b}" shows "x \ {v <--< b}" proof - have "v \ x" by (smt dist_commute x(1)) moreover have "x \ {a<-- {a<--_limit_points: assumes transversal: "transversal_segment a b" assumes ex_pos: "{0..} \ existence_ivl0 x" assumes u: "\_limit_point x u" "u \ {a<--_limit_point x v" "v \ {a<-- {u<-- v" using uv using dist_in_open_segment by blast define duv where "duv = dist u v / 2" have duv: "duv > 0" unfolding duv_def using unotv by simp from \_limit_crossings[OF transversal ex_pos u] obtain su where su: "filterlim su at_top sequentially" "(flow0 x \ su) \ u" "\\<^sub>F n in sequentially. flow0 x (su n) \ {a<-- su n \ existence_ivl0 x" by blast from \_limit_crossings[OF transversal ex_pos v] obtain sv where sv: "filterlim sv at_top sequentially" "(flow0 x \ sv) \ v" "\\<^sub>F n in sequentially. flow0 x (sv n) \ {a<-- sv n \ existence_ivl0 x" by blast from filterlim_at_top_tendstoE[OF duv su] obtain su1 where su1:"su1 > 0" "flow0 x su1 \ {a<-- existence_ivl0 x" "dist (flow0 x su1) u < duv" by auto from filterlim_at_top_tendstoE[OF duv sv, of su1] obtain su2 where su2:"su2 > su1" "flow0 x su2 \ {a<-- existence_ivl0 x" "dist (flow0 x su2) v < duv" by auto from filterlim_at_top_tendstoE[OF duv su, of su2] obtain su3 where su3:"su3 > su2" "flow0 x su3 \ {a<-- existence_ivl0 x" "dist (flow0 x su3) u < duv" by auto have *: "su1 \ su2" "{su1..su2} \ existence_ivl0 x" using su1 su2 apply linarith by (metis atLeastatMost_empty_iff empty_iff mvar.closed_segment_subset_domain real_Icc_closed_segment su1(3) su2(3) subset_eq) (* by construction *) have d1: "dist (flow0 x su1) v \ (dist u v)/2" using su1(4) duv unfolding duv_def by (smt dist_triangle_half_r) have "dist (flow0 x su1) u < dist u v" using su1(4) duv unfolding duv_def by linarith from open_segment_separate_left[OF u(2) uv this su1(2)] have su1l:"flow0 x su1 \ {a<-- {flow0 x su1<-- {u<-- (dist u v)/2" using su2(4) duv unfolding duv_def by (smt dist_triangle_half_r) then have "dist (flow0 x su3) u < dist u (flow0 x su2)" by (smt dist_commute duv_def su3(4)) from open_segment_separate_left[OF u(2) su2ll this su3(2)] have su3l:"flow0 x su3 \ {a<-- {a <--Unique Intersection\ text \Perko Section 3.7 Remark 2\ lemma unique_transversal_segment_intersection: assumes "transversal_segment a b" assumes "{0..} \ existence_ivl0 x" assumes "u \ \_limit_set x \ {a<--_limit_set x \ {a<--_limit_set x \ {a<-- {u}" then obtain v where uv: "u \ v" and v: "\_limit_point x v" "v \ {a<--_limit_set_def by fastforce have u:"\_limit_point x u" "u \ {a<--_limit_set_def by auto show False using no_two_\_limit_points[OF \transversal_segment a b\] by (smt dist_commute dist_in_open_segment open_segment_trichotomy u uv v assms) qed text \Adapted from Perko Section 3.7 Lemma 4 (+ Chicone )\ lemma periodic_imp_\_limit_set: assumes "compact K" "K \ X" assumes "x \ X" "trapped_forward x K" assumes "periodic_orbit y" "flow0 y ` UNIV \ \_limit_set x" shows "flow0 y `UNIV = \_limit_set x" proof (rule ccontr) note y = \periodic_orbit y\ \flow0 y ` UNIV \ \_limit_set x\ from trapped_sol_right[OF assms(1-4)] have ex_pos: "{0..} \ existence_ivl0 x" by blast assume "flow0 y `UNIV \ \_limit_set x" obtain p where p: "p \ \_limit_set x" "p \ flow0 y ` UNIV" using y(2) apply auto using \range (flow0 y) \ \_limit_set x\ by blast from \_limit_set_in_compact_connected[OF assms(1-4)] have wcon: "connected (\_limit_set x)" . from \_limit_set_invariant have "invariant (\_limit_set x)" . from \_limit_set_in_compact_compact[OF assms(1-4)] have "compact (\_limit_set x)" . then have sc: "seq_compact (\_limit_set x)" using compact_imp_seq_compact by blast have y1:"closed (flow0 y ` UNIV)" using closed_orbit_\_limit_set periodic_orbit_def \_limit_set_closed y(1) by auto have y2: "flow0 y ` UNIV \ {}" by simp let ?py = "infdist p (range (flow0 y))" have "0 < ?py" using y1 y2 p(2) by (rule infdist_pos_not_in_closed) have "\n::nat. \z. z \ \_limit_set x - flow0 y ` UNIV \ infdist z (flow0 y ` UNIV) < ?py/2^n" proof (rule ccontr) assume " \ (\n. \z. z \ \_limit_set x - range (flow0 y) \ infdist z (range (flow0 y)) < infdist p (range (flow0 y)) / 2 ^ n) " then obtain n where n: "(\z \ \_limit_set x - range (flow0 y). infdist z (range (flow0 y)) \ ?py / 2 ^ n)" using not_less by blast define A where "A = flow0 y ` UNIV" define B where "B = {z. infdist z (range (flow0 y)) \ ?py / 2 ^ n}" have Ac:"closed A" unfolding A_def using y1 by auto have Bc:"closed B" unfolding B_def using infdist_closed by auto have "A \ B = {}" proof (rule ccontr) assume "A \ B \ {}" then obtain q where q: "q \ A" "q \ B" by blast have qz:"infdist q (range(flow0 y)) = 0" using q(1) unfolding A_def by simp note \0 < ?py\ moreover have "2 ^ n > (0::real)" by auto ultimately have "infdist p (range (flow0 y)) / 2 ^ n > (0::real)" by simp then have qnz: "infdist q(range (flow0 y)) > 0" using q(2) unfolding B_def by auto show False using qz qnz by auto qed then have a1:"A \ B \ \_limit_set x = {}" by auto have "\_limit_set x - range(flow0 y) \ B" using n B_def by blast then have a2:"\_limit_set x \ A \ B" using A_def by auto from connected_closedD[OF wcon a1 a2 Ac Bc] have "A \ \_limit_set x = {} \ B \ \_limit_set x = {}" . moreover { assume "A \ \_limit_set x = {}" then have False unfolding A_def using y(2) by blast } moreover { assume "B \ \_limit_set x = {}" then have False unfolding B_def using p using A_def B_def a2 by blast } ultimately show False by blast qed then obtain s where s: "\n::nat. (s::nat \ _) n \ \_limit_set x - flow0 y ` UNIV \ infdist (s n) (flow0 y ` UNIV) < ?py/2^n" by metis then have "\n. s n \ \_limit_set x" by blast from seq_compactE[OF sc this] obtain l r where lr: "l \ \_limit_set x" "strict_mono r" "(s \ r) \ l" by blast have "\n. infdist (s n) (range (flow0 y)) \ ?py / 2 ^ n" using s using less_eq_real_def by blast then have "\n. norm(infdist (s n) (range (flow0 y))) \ ?py / 2 ^ n" by (auto simp add: infdist_nonneg) from LIMSEQ_norm_0_pow[OF \0 < ?py\ _ this] have "((\z. infdist z (flow0 y ` UNIV)) \ s) \ 0" by (auto simp add:o_def) from LIMSEQ_subseq_LIMSEQ[OF this lr(2)] have "((\z. infdist z (flow0 y ` UNIV)) \ (s \ r)) \ 0" by (simp add: o_assoc) moreover have "((\z. infdist z (flow0 y ` UNIV)) \ (s \ r)) \ infdist l (flow0 y ` UNIV)" - using continuous_on_sequentially lr(3) continuous_on_infdist - by blast + by (auto intro!: tendsto_eq_intros tendsto_compose_at[OF lr(3)]) ultimately have "infdist l (flow0 y `UNIV) = 0" using LIMSEQ_unique by auto then have lu: "l \ flow0 y ` UNIV" using in_closed_iff_infdist_zero[OF y1 y2] by auto then have l1:"l \ X" using closed_orbit_global_existence periodic_orbit_def y(1) by auto (* TODO: factor out as periodic_orbitE *) have l2:"f l \ 0" by (smt \l \ X\ \l \ range (flow0 y)\ closed_orbit_global_existence fixed_point_imp_closed_orbit_period_zero(2) fixpoint_sol(2) image_iff local.flows_reverse periodic_orbit_def y(1)) from transversal_segment_exists[OF l1 l2] obtain a b where ab: "transversal_segment a b" "l \ {a<-- \_limit_set x \ {a<--_limit_set x \ {a<--y. y \ ball l d \ flow0 y (t y) \ {a<--y. y \ ball l d \ \t y\ < 1)" "continuous_on (ball l d) t" "t l = 0" by auto obtain n where "(s \ r) n \ ball l d" using lr(3) dt(1) unfolding LIMSEQ_iff_nz by (metis dist_commute mem_ball order_refl) then have "flow0 ((s \ r) n) (t ((s \ r) n )) \ {a<-- r) n \ \_limit_set x" "(s \ r) n \ flow0 y ` UNIV" using s by auto moreover have "flow0 ((s \ r) n) (t ((s \ r) n )) \ \_limit_set x" using \invariant (\_limit_set x)\ calculation unfolding invariant_def trapped_def by (smt \_limit_set_in_compact_subset \invariant (\_limit_set x)\ assms(1-4) invariant_def order_trans range_eqI subsetD trapped_iff_on_existence_ivl0 trapped_sol) ultimately have "flow0 ((s \ r) n) (t ((s \ r) n )) \ \_limit_set x \ {a<-- r) n) (t ((s \ r) n )) = l" using luniq by auto then have "((s \ r) n) = flow0 l (-(t ((s \ r) n ))) " by (smt UNIV_I \(s \ r) n \ \_limit_set x\ flows_reverse \_limit_set_in_compact_existence assms(1-4)) thus False using sr(2) lu \flow0 ((s \ r) n) (t ((s \ r) n)) = l\ \flow0 ((s \ r) n) (t ((s \ r) n)) \ \_limit_set x\ closed_orbit_global_existence image_iff local.flow_trans periodic_orbit_def \_limit_set_in_compact_existence range_eqI assms y(1) by smt qed end context c1_on_open_R2 begin lemma \_limit_crossings: assumes "transversal_segment a b" assumes pos_ex: "{..0} \ existence_ivl0 x" assumes "\_limit_point x p" assumes "p \ {a<--\<^bsub>\<^esub> -\" "(flow0 x \ s) \ p" "\\<^sub>F n in sequentially. flow0 x (s n) \ {a<-- s n \ existence_ivl0 x" proof - from pos_ex have "{0..} \ uminus ` existence_ivl0 x" by force from rev.\_limit_crossings[unfolded rev_transversal_segment rev_existence_ivl_eq0 rev_eq_flow \_limit_point_eq_rev[symmetric], OF assms(1) this assms(3,4)] obtain s where "filterlim s at_top sequentially" "((\t. flow0 x (- t)) \ s) \ p" "\\<^sub>F n in sequentially. flow0 x (- s n) \ {a<-- s n \ uminus ` existence_ivl0 x" . then have "filterlim (-s) at_bot sequentially" "(flow0 x \ (-s)) \ p" "\\<^sub>F n in sequentially. flow0 x ((-s) n) \ {a<-- (-s) n \ existence_ivl0 x" by (auto simp: fun_Compl_def o_def filterlim_uminus_at_top) then show ?thesis .. qed text \If a positive limit point has a regular point in its positive limit set then it is periodic\ lemma \_limit_point_\_limit_set_regular_imp_periodic: assumes "compact K" "K \ X" assumes "x \ X" "trapped_forward x K" assumes y: "y \ \_limit_set x" "f y \ 0" assumes z: "z \ \_limit_set y \ \_limit_set y" "f z \ 0" shows "periodic_orbit y \ flow0 y ` UNIV = \_limit_set x" proof - from trapped_sol_right[OF assms(1-4)] have ex_pos: "{0..} \ existence_ivl0 x" by blast from \_limit_set_in_compact_existence[OF assms(1-4) y(1)] have yex: "existence_ivl0 y = UNIV" . from \_limit_set_invariant have "invariant (\_limit_set x)" . then have yinv: "flow0 y ` UNIV \ \_limit_set x" using yex unfolding invariant_def using trapped_iff_on_existence_ivl0 y(1) by blast have zy: "\_limit_point y z \ \_limit_point y z" using z unfolding \_limit_set_def \_limit_set_def by auto from \_limit_set_in_compact_\_limit_set_contained[OF assms(1-4)] \_limit_set_in_compact_\_limit_set_contained[OF assms(1-4)] have zx:"z \ \_limit_set x" using zy y using z(1) by blast then have "z \ X" by (metis UNIV_I local.existence_ivl_initial_time_iff \_limit_set_in_compact_existence assms(1-4)) from transversal_segment_exists[OF this z(2)] obtain a b where ab: "transversal_segment a b" "z \ {a<-- {a<-- {a<-- t2" proof assume zy: "\_limit_point y z" from \_limit_crossings[OF ab(1) _ zy ab(2), unfolded yex] obtain s where s: "filterlim s at_top sequentially" "(flow0 y \ s) \ z" "\\<^sub>F n in sequentially. flow0 y (s n) \ {a<-- {a<--\<^sub>F n in sequentially. s n > t1" using filterlim_at_top_dense s(1) by auto with s(3) have "\\<^sub>F n in sequentially. flow0 y (s n) \ {a<-- s n > t1" by eventually_elim simp from eventually_happens[OF this] obtain t2 where t2: "flow0 y t2 \ {a<-- t2" by auto from t1 this show ?thesis .. next assume zy: "\_limit_point y z" from \_limit_crossings[OF ab(1) _ zy ab(2), unfolded yex] obtain s where s: "filterlim s at_bot sequentially" "(flow0 y \ s) \ z" "\\<^sub>F n in sequentially. flow0 y (s n) \ {a<-- {a<--\<^sub>F n in sequentially. s n < t1" using filterlim_at_bot_dense s(1) by auto with s(3) have "\\<^sub>F n in sequentially. flow0 y (s n) \ {a<-- s n < t1" by eventually_elim simp from eventually_happens[OF this] obtain t2 where t2: "flow0 y t2 \ {a<-- t2" by auto from t1 this show ?thesis .. qed have "flow0 y t1 \ \_limit_set x \ {a<-- \_limit_set x \ {a<--transversal_segment a b\ ex_pos] by blast have "t1 \ t2" "t1 \ existence_ivl0 y" "t2 \ existence_ivl0 y" using \t1 \ t2\ apply blast apply (simp add: yex) by (simp add: yex) from periodic_orbitI[OF this feq y(2)] have 1: "periodic_orbit y" . from periodic_imp_\_limit_set[OF assms(1-4) this yinv] have 2: "flow0 y` UNIV = \_limit_set x" . show ?thesis using 1 2 by auto qed subsection \Poincare Bendixson Theorems\ text \Perko Section 3.7 Theorem 1\ theorem poincare_bendixson: assumes "compact K" "K \ X" assumes "x \ X" "trapped_forward x K" assumes "0 \ f ` (\_limit_set x)" obtains y where "periodic_orbit y" "flow0 y ` UNIV = \_limit_set x" proof - note f = \0 \ f ` (\_limit_set x)\ from \_limit_set_in_compact_nonempty[OF assms(1-4)] obtain y where y: "y \ \_limit_set x" by fastforce from \_limit_set_in_compact_existence[OF assms(1-4) y] have yex: "existence_ivl0 y = UNIV" . from \_limit_set_invariant have "invariant (\_limit_set x)" . then have yinv: "flow0 y ` UNIV \ \_limit_set x" using yex unfolding invariant_def using trapped_iff_on_existence_ivl0 y by blast from \_limit_set_in_compact_subset[OF assms(1-4)] have "\_limit_set x \ K" . then have "flow0 y ` UNIV \ K" using yinv by auto then have yk:"trapped_forward y K" by (simp add: image_subsetI range_subsetD trapped_forward_def) have "y \ X" by (simp add: local.mem_existence_ivl_iv_defined(2) yex) from \_limit_set_in_compact_nonempty[OF assms(1-2) this _] obtain z where z: "z \ \_limit_set y" using yk by blast from \_limit_set_in_compact_\_limit_set_contained[OF assms(1-4)] have zx:"z \ \_limit_set x" using \z \ \_limit_set y\ y by auto have yreg : "f y \ 0" using f y by (metis rev_image_eqI) have zreg : "f z \ 0" using f zx by (metis rev_image_eqI) from \_limit_point_\_limit_set_regular_imp_periodic[OF assms(1-4) y yreg _ zreg] z show ?thesis using that by blast qed lemma fixed_point_in_\_limit_set_imp_\_limit_set_singleton_fixed_point: assumes "compact K" "K \ X" assumes "x \ X" "trapped_forward x K" assumes fp: "yfp \ \_limit_set x" "f yfp = 0" assumes zpx: "z \ \_limit_set x" assumes finite_fp: "finite {y \ K. f y = 0}" (is "finite ?S") shows "(\p1 \ \_limit_set x. f p1 = 0 \ \_limit_set z = {p1}) \ (\p2 \ \_limit_set x. f p2 = 0 \ \_limit_set z = {p2})" proof - let ?weq = "{y \ \_limit_set x. f y = 0}" from \_limit_set_in_compact_subset[OF assms(1-4)] have wxK: "\_limit_set x \ K" . from \_limit_set_in_compact_\_limit_set_contained[OF assms(1-4)] have zx: "\_limit_set z \ \_limit_set x" using zpx by auto have zX: "z \ X" using subset_trans[OF wxK assms(2)] by (metis subset_iff zpx) from \_limit_set_in_compact_subset[OF assms(1-4)] have "?weq \ ?S" by (smt Collect_mono_iff Int_iff inf.absorb_iff1) then have "finite ?weq" using \finite ?S\ by (blast intro: rev_finite_subset) consider "f z = 0" | "f z \ 0" by auto then show ?thesis proof cases assume "f z = 0" from fixed_point_imp_\_limit_set[OF zX this] fixed_point_imp_\_limit_set[OF zX this] show ?thesis by (metis (mono_tags) \f z = 0\ zpx) next assume "f z \ 0" have zweq: "\_limit_set z \ ?weq" apply clarsimp proof (rule ccontr) fix k assume k: "k \ \_limit_set z" "\ (k \ \_limit_set x \ f k = 0)" then have "f k \ 0" using zx k by auto from \_limit_point_\_limit_set_regular_imp_periodic[OF assms(1-4) zpx \f z \ 0\ _ this] k(1) have "periodic_orbit z" "range(flow0 z) = \_limit_set x" by auto then have "0 \ f ` (\_limit_set x)" by (metis image_iff periodic_orbit_imp_flow0_regular) thus False using fp by (metis (mono_tags, lifting) empty_Collect_eq image_eqI) qed have zweq0: "\_limit_set z \ ?weq" apply clarsimp proof (rule ccontr) fix k assume k: "k \ \_limit_set z" "\ (k \ \_limit_set x \ f k = 0)" then have "f k \ 0" using zx k \_limit_set_in_compact_\_limit_set_contained[OF assms(1-4), of z] zpx by auto from \_limit_point_\_limit_set_regular_imp_periodic[OF assms(1-4) zpx \f z \ 0\ _ this] k(1) have "periodic_orbit z" "range(flow0 z) = \_limit_set x" by auto then have "0 \ f ` (\_limit_set x)" by (metis image_iff periodic_orbit_imp_flow0_regular) thus False using fp by (metis (mono_tags, lifting) empty_Collect_eq image_eqI) qed from \_limit_set_in_compact_existence[OF assms(1-4) zpx] have zex: "existence_ivl0 z = UNIV" . from \_limit_set_invariant have "invariant (\_limit_set x)" . then have zinv: "flow0 z ` UNIV \ \_limit_set x" using zex unfolding invariant_def using trapped_iff_on_existence_ivl0 zpx by blast then have "flow0 z ` UNIV \ K" using wxK by auto then have a2: "trapped_forward z K" "trapped_backward z K" using trapped_def trapped_iff_on_existence_ivl0 apply fastforce using \range (flow0 z) \ K\ trapped_def trapped_iff_on_existence_ivl0 by blast have a3: "finite (\_limit_set z)" by (metis \finite ?weq\ finite_subset zweq) from finite_\_limit_set_in_compact_imp_unique_fixed_point[OF assms(1-2) zX a2(1) a3] obtain p1 where p1: "\_limit_set z = {p1}" "f p1 = 0" by blast then have "p1 \ ?weq" using zweq by blast moreover have "finite (\_limit_set z)" by (metis \finite ?weq\ finite_subset zweq0) from finite_\_limit_set_in_compact_imp_unique_fixed_point[OF assms(1-2) zX a2(2) this] obtain p2 where p2: "\_limit_set z = {p2}" "f p2 = 0" by blast then have "p2 \ ?weq" using zweq0 by blast ultimately show ?thesis by (simp add: p1 p2) qed qed end context c1_on_open_R2 begin text \Perko Section 3.7 Theorem 2\ theorem poincare_bendixson_general: assumes "compact K" "K \ X" assumes "x \ X" "trapped_forward x K" assumes "S = {y \ K. f y = 0}" "finite S" shows "(\y \ S. \_limit_set x = {y}) \ (\y. periodic_orbit y \ flow0 y ` UNIV = \_limit_set x) \ (\P R. \_limit_set x = P \ R \ P \ S \ 0 \ f ` R \ R \ {} \ (\z \ R. (\p1 \ P. \_limit_set z = {p1}) \ (\p2 \ P. \_limit_set z = {p2})))" proof - note S = \S = {y \ K. f y = 0}\ let ?wreg = "{y \ \_limit_set x. f y \ 0}" let ?weq = "{y \ \_limit_set x. f y = 0}" have wreqweq: "?wreg \ ?weq = \_limit_set x" by (smt Collect_cong Collect_disj_eq mem_Collect_eq \_limit_set_def) from trapped_sol_right[OF assms(1-4)] have ex_pos: "{0..} \ existence_ivl0 x" by blast from \_limit_set_in_compact_subset[OF assms(1-4)] have wxK: "\_limit_set x \ K" . then have "?weq \ S" using S by (smt Collect_mono_iff Int_iff inf.absorb_iff1) then have "finite ?weq" using \finite S\ by (metis rev_finite_subset) from \_limit_set_invariant have xinv: "invariant (\_limit_set x)" . from \_limit_set_in_compact_nonempty[OF assms(1-4)] wreqweq consider "?wreg = {}" | "?weq = {}" | "?weq \ {}" "?wreg \ {}" by auto then show ?thesis proof cases (* If w has no regular points then it is equal to a single unique fixed point *) assume "?wreg = {}" then have "finite (\_limit_set x)" by (metis (mono_tags, lifting) \{y \ \_limit_set x. f y = 0} \ S\ \finite S\ rev_finite_subset sup_bot.left_neutral wreqweq) from finite_\_limit_set_in_compact_imp_unique_fixed_point[OF assms(1-4) this] obtain y where y: "\_limit_set x = {y}" "f y = 0" by blast then have "y \ S" by (metis Un_empty_left \?weq \ S\ \?wreg = {}\ insert_subset wreqweq) then show ?thesis using y by auto next (* If w has no fixed points, then the Poincare Bendixson theorem applies *) assume "?weq = {}" then have " 0 \ f ` \_limit_set x" by (smt empty_Collect_eq imageE) from poincare_bendixson[OF assms(1-4) this] have "(\y. periodic_orbit y \ flow0 y ` UNIV = \_limit_set x)" by metis then show ?thesis by blast next (* Otherwise, all points in the limit set converge to a finite subset of the fixed points *) assume "?weq \ {}" "?wreg \ {}" then obtain yfp where yfp: "yfp \ \_limit_set x" "f yfp = 0" by auto have "0 \ f ` ?wreg" by auto have "(\p1\\_limit_set x. f p1 = 0 \ \_limit_set z = {p1}) \ (\p2\\_limit_set x. f p2 = 0 \ \_limit_set z = {p2})" if zpx: "z \ \_limit_set x" for z using fixed_point_in_\_limit_set_imp_\_limit_set_singleton_fixed_point[ OF assms(1-4) yfp zpx \finite S\[unfolded S]] by auto then have "\_limit_set x = ?weq \ ?wreg \ ?weq \ S \ 0 \ f ` ?wreg \ ?wreg \ {} \ (\z \ ?wreg. (\p1 \ ?weq. \_limit_set z = {p1}) \ (\p2 \ ?weq. \_limit_set z = {p2}))" using wreqweq \?weq \ S\ \?wreg \ {}\ \0 \ f ` ?wreg\ by blast then show ?thesis by blast qed qed corollary poincare_bendixson_applied: assumes "compact K" "K \ X" assumes "K \ {}" "positively_invariant K" assumes "0 \ f ` K" obtains y where "periodic_orbit y" "flow0 y ` UNIV \ K" proof - from assms(1-4) obtain x where "x \ K" "x \ X" by auto have *: "trapped_forward x K" using assms(4) \x \ K\ by (auto simp: positively_invariant_def) have subs: "\_limit_set x \ K" by (rule \_limit_set_in_compact_subset[OF assms(1-2) \x \ X\ *]) with assms(5) have "0 \ f ` \_limit_set x" by auto from poincare_bendixson[OF assms(1-2) \x \ X\ * this] obtain y where "periodic_orbit y" "range (flow0 y) = \_limit_set x" by force then have "periodic_orbit y" "flow0 y ` UNIV \ K" using subs by auto then show ?thesis .. qed (* Limit cycles are periodic orbits that is the \ (or \)-limit set of some point not in the cycle. As with periodic_orbit, limit_cycles are defined for a representative point y *) definition "limit_cycle y \ periodic_orbit y \ (\x. x \ flow0 y ` UNIV \ (flow0 y ` UNIV = \_limit_set x \ flow0 y ` UNIV = \_limit_set x))" corollary poincare_bendixson_limit_cycle: assumes "compact K" "K \ X" assumes "x \ K" "positively_invariant K" assumes "0 \ f ` K" assumes "rev.flow0 x t \ K" obtains y where "limit_cycle y" "flow0 y ` UNIV \ K" proof - have "x \ X" using assms(2-3) by blast have *: "trapped_forward x K" using assms(3-4) by (auto simp: positively_invariant_def) have subs: "\_limit_set x \ K" by (rule \_limit_set_in_compact_subset[OF assms(1-2) \x \ X\ *]) with assms(5) have "0 \ f ` \_limit_set x" by auto from poincare_bendixson[OF assms(1-2) \x \ X\ * this] obtain y where y: "periodic_orbit y" "range (flow0 y) = \_limit_set x" by force then have c2: "flow0 y ` UNIV \ K" using subs by auto have exy: "existence_ivl0 y = UNIV" using closed_orbit_global_existence periodic_orbit_def y(1) by blast have "x \ flow0 y ` UNIV" proof clarsimp fix tt assume "x = flow0 y tt" then have "rev.flow0 (flow0 y tt) t \ K" using assms(6) by auto moreover have "rev.flow0 (flow0 y tt) t \ flow0 y ` UNIV" using exy unfolding rev_eq_flow using UNIV_I \x = flow0 y tt\ closed_orbit_\_limit_set closed_orbit_flow0 periodic_orbit_def y by auto ultimately show False using c2 by blast qed then have "limit_cycle y" "flow0 y ` UNIV \ K" using y c2 unfolding limit_cycle_def by auto then show ?thesis .. qed end end