Theory Poincare_Bendixson
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
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'}"
unfolding flow_to_path_def image_comp[symmetric] linepath_image0_right_open_real[OF assms]
by auto
lemma flow_to_path_path:
assumes "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<..<t'}. flow0 x s ≠ 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<--<y} for the open segment›
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$⇩e0 - y$⇩e0, x$⇩e1 - y$⇩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 *⇩R v) = u *⇩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 *⇩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 *⇩R (b - a))"
if "(x - a) ∙ rot (b - a) = 0" "a ≠ b"
proof -
from that have
x0: "b $⇩e 0 = a $⇩e 0 ⟹ x $⇩e 0 =
(a $⇩e 0 * b $⇩e Suc 0 - b $⇩e 0 * a $⇩e Suc 0 + (b $⇩e 0 - a $⇩e 0) * x $⇩e Suc 0) /
(b $⇩e Suc 0 - a $⇩e Suc 0)"
and x1: "b $⇩e 0 ≠ a $⇩e 0 ⟹ x $⇩e Suc 0 =
((b $⇩e Suc 0 - a $⇩e Suc 0) * x $⇩e 0 - a $⇩e 0 * b $⇩e Suc 0 + b $⇩e 0 * a $⇩e Suc 0) / (b $⇩e 0 - a $⇩e 0)"
by (auto simp: rot_def vec_simps divide_simps)
define u where "u = (if b $⇩e 0 - a $⇩e 0 ≠ 0
then ((x $⇩e 0 - a $⇩e 0) / (b $⇩e 0 - a $⇩e 0))
else ((x $⇩e 1 - a $⇩e 1) / (b $⇩e 1 - a $⇩e 1)))
"
show ?thesis
apply (cases "b $⇩e 0 - a $⇩e 0 = 0")
subgoal
using that(2)
apply (auto intro!: image_eqI[where x="((x $⇩e 1 - a $⇩e 1) / (b $⇩e 1 - a $⇩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 $⇩e 0 - a $⇩e 0) / (b $⇩e 0 - a $⇩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<--<b} ⟷ (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<--<b} ⟹ (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 *⇩R (b - a)" "0 ≤ u" "u ≤ 1"
by (auto simp: in_segment algebra_simps)
from that obtain v where y: "y = a + v *⇩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$⇩e0 + 𝗂 * x$⇩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
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<--<b}"
shows "∀⇩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 ∙ (b - a)}"
unfolding in_open_segment_iff_rot[OF ‹a ≠ b›]
by auto
then have "∀⇩F y in at x. y ∙ (b - a) ∈ {a ∙ (b - a)<..<b ∙ (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<--<b}"
obtains e where "e > 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<--<b}"
by (force simp: eventually_at in_open_segment_iff_rot dist_commute)
then show ?thesis ..
qed
lemma linepath_ball_inside_outside:
fixes p :: "real ⇒ 'a"
assumes jordan: "simple_path (p +++ linepath a b)" "pathfinish p = a" "pathstart p = b"
assumes x: "x ∈ {a<--<b}"
obtains e where "e > 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 "∀⇩F y in at x. y ∉ path_image p"
by (intro eventually_not_in_closed) (auto simp: closed_path_image ‹path p›)
moreover
have "∀⇩F y in at x. (y - a) ∙ rot (a - b) = 0 ⟶ y ∈ {a<--<b}"
by (rule eventually_at_open_segment[OF x])
ultimately have "∀⇩F y in at x. y ∉ path_image p ∧ ((y - a) ∙ rot (a - b) = 0 ⟶ y ∈ {a<--<b})"
by eventually_elim auto
then obtain e where e: "e > 0" "ball x e ∩ path_image p = {}"
"ball x e ∩ {y. (y - a) ∙ rot (a - b) = 0} ⊆ {a<--<b}"
using ‹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<--<b}" unfolding b3_def using e by blast
then have "z ∈ 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<--<b}" unfolding b3_def using e by auto
then have "y ∈ 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›
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, opaque_lifting) 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 *⇩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) *⇩R x + u *⇩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 *⇩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 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 *⇩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<--<b}"
"transversal_segment a b"
proof -
define l where "l = (λs::real. x + (s/norm(f x)) *⇩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
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) *⇩R (l (-dr)) + u *⇩R (l dr)"
unfolding in_segment by blast
then have "z = x - (1-u) *⇩R (dr/norm(f x)) *⇩R rot (f x) + u *⇩R (dr/norm(f x)) *⇩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) *⇩R (dr/norm(f x)) *⇩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)) *⇩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 *⇩R (dr/norm(f x)) *⇩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)) *⇩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 "∀⇩F x in at x. ?a x > 0"
by (rule order_tendstoD)
moreover have "∀⇩F x in at x. x ∈ X"
by (rule topological_tendstoD[OF tendsto_ident_at open_dom ‹x ∈ X›])
moreover have "∀⇩F x in at x. f x ≠ 0"
by (rule tendsto_imp_eventually_ne tendsto_intros ‹x ∈ X› ‹f x ≠ 0›)+
ultimately have "∀⇩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 "∀⇩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+
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: 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: 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) *⇩R a + u *⇩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) *⇩R a + u *⇩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<--<b}"
assumes "x2 ∈ {x1<--<b}"
shows "(y ∙ 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 *⇩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<--<b}"
assumes x2: "flow0 x t2 ∈ {flow0 x t1<--<b}"
assumes "⋀t. t ∈ {t1<..<t2} ⟹ flow0 x t ∉ {a<--<b}"
assumes "t > t2" "t ∈ existence_ivl0 x"
shows "flow0 x t ∉ {a<--<flow0 x t2}"
proof -
note exist = ‹{t1..t2} ⊆ existence_ivl0 x›
note t1t2 = ‹⋀t. t ∈ {t1<..<t2} ⟹ flow0 x t ∉ {a<--<b}›
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<--<b}"
by (simp add: open_closed_segment subset_open_segment x1)
have t12sub: "{flow0 x t1--flow0 x t2} ⊆ {a<--<b}"
by (metis ends_in_segment(2) open_closed_segment subset_co_segment subset_eq subset_open_segment x1 x2)
have subr: "{flow0 x t1<--<flow0 x t2} ⊆ {flow0 x t1 <--<b}"
by (simp add: open_closed_segment subset_open_segment x2)
have "flow0 x t1 ∈ {a <--<flow0 x t2}" using x1 x2
by (rule open_segment_subsegment)
then have subl: "{flow0 x t1<--<flow0 x t2} ⊆ {a <--< flow0 x t2}" using x1 x2
by (simp add: open_closed_segment subset_open_segment x2)
then have subl2: "{flow0 x t1--<flow0 x t2} ⊆ {a <--< flow0 x t2}" using x1 x2
by (smt DiffE DiffI ‹flow0 x t1 ∈ {a<--<flow0 x t2}› 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<--<flow0 x t2} ⊆ {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<--<flow0 x t2}› open_closed_segment subset_closed_segment)
then have suba12_open: "{a<--<flow0 x t1} ⊆ {a<--<flow0 x t2}"
using x2_notmem
by (auto simp: open_segment_def)
have "flow0 x t2 ∈ {a--b}"
using suba2 by auto
have intereq: "⋀t. t1 ≤ t ⟹ t ≤ t2 ⟹ flow0 x t ∈ {a<--<b} ⟹ t = t1 ∨ t = t2"
proof (rule ccontr)
fix t
assume t: "t1 ≤ t" "t ≤ t2" "flow0 x t ∈ {a<--<b}" "¬(t= t1 ∨ t = t2)"
then have "t ∈ {t1<..<t2}" by auto
then have "flow0 x t ∉ {a<--<b}" using t1t2 by blast
thus False using t by auto
qed
then have intereqt12: "⋀t. t1 ≤ t ⟹ t ≤ t2 ⟹ flow0 x t ∈ {flow0 x t1--flow0 x t2} ⟹ t = t1 ∨ t = t2"
using t12sub by blast
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"
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 <--<flow0 x t2}"
unfolding piJ J1_def J2_def path_image_flow_to_path[OF ‹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<..<t2}. flow0 x s ≠ 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..<T}. flow0 y s ∈ side2) ∧
flow0 y T ∈ {flow0 x t1--<flow0 x t2}"
if "side1 ∩ 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..<u*t}. flow0 y s ∈ 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..<u*t}" unfolding sc_def by (simp add: st1 c1 s(1))
then have "u*t - sc ∈ 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..<T}. flow0 y s ∈ side2) ∧
flow0 y T ∈ {flow0 x t1--<flow0 x t2}"
using c1 c2 c3 c4 unfolding piD
by (metis DiffE UnE ends_in_segment(1) half_open_segment_closed_segmentI insertCI open_segment_def x1neqx2)
qed
have outside_in: "⋀y t. y ∈ outer ⟹
0 ≤ t ⟹ t ∈ existence_ivl0 y ⟹
flow0 y t ∈ closure inner ⟹
∃T. 0 < T ∧ T ≤ t ∧ (∀s ∈{0..<T}. flow0 y s ∈ outer) ∧
flow0 y T ∈ {flow0 x t1--<flow0 x t2}"
by (rule swap_side; (rule io | assumption))
have inside_out: "⋀y t. y ∈ inner ⟹
0 ≤ t ⟹ t ∈ existence_ivl0 y ⟹
flow0 y t ∈ closure outer ⟹
∃T. 0 < T ∧ T ≤ t ∧ (∀s ∈{0..<T}. flow0 y s ∈ inner) ∧
flow0 y T ∈ {flow0 x t1--<flow0 x t2}"
by (rule swap_side; (rule io2 io | assumption))
from leaves_transversal_segmentE[OF assms(1)]
obtain d n where d: "d > (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)
define r1 where "r1 = (λ(x, y). flow0 x y)`({flow0 x t1<--<b} × {0<..<d}) "
have r1a1: "path_connected {flow0 x t1 <--<b}" by simp
have r1a2: "path_connected {0<..<d}" by simp
have "{flow0 x t1<--<b} ⊆ {a--b}"
by (simp add: open_closed_segment subset_oc_segment x1)
then have r1a3: "y ∈ {flow0 x t1<--<b} ⟹ {0<..<d} ⊆ 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<--<b}"
and ss: "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<--<b}"
apply (subst flow_trans[symmetric])
apply fact
subgoal using neg_tt_ex eq by simp
apply (rule t1t2)
using 1 ss tt
unfolding e_def
by auto
moreover have "flow0 (flow0 x ss) (-tt) ∈ {a<--<b}"
unfolding eq[symmetric] using tt_ex xx
apply (subst flow_trans[symmetric])
apply (auto simp add: neg_tt_ex)
by (metis (no_types, opaque_lifting) sub1b subset_eq subset_open_segment)
ultimately show ?thesis by simp
next
case 2
have les: "0 ≤ 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
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<--<flow0 x t2}› suba2o by auto
qed
qed
qed
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<--<b}" "ba ∈ {0<..<d}"
with sub1b show "0 < (flow0 aa ba - a) ∙ 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<--<flow0 x t2}"
and ss: "t1 ≤ 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<--<b}"
apply (subst flow_trans[symmetric])
apply fact
subgoal using neg_tt_ex eq by simp
apply (rule t1t2)
using 1 ss tt
unfolding e_def
by auto
moreover have "flow0 (flow0 x ss) (-tt) ∈ {a<--<b}"
unfolding eq[symmetric] using tt_ex xx
apply (subst flow_trans[symmetric])
apply (auto simp add: neg_tt_ex)
by (metis (no_types, opaque_lifting) suba2 subset_eq subset_open_segment)
ultimately show ?thesis by simp
next
case 2
have les: "tt + e ≤ 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
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<--<flow0 x t2}" "ba ∈ {-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<--<flow0 x t2}" unfolding rp_def
by (simp add: x1neqx2)
have "rp ∈ {a -- b}"
using rpi suba2o subl by blast
then have [simp]: "rp ∈ X"
using ‹{a--b} ⊆ X› by blast
have *: "pathfinish J1 = flow0 x t2"
"pathstart J1 = flow0 x t1"
"rp ∈ {flow0 x t2<--<flow0 x t1}"
using rpi
by (auto simp: open_segment_commute J1_def)
have "{y. 0 < (y - 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 "∀⇩F t in at_right 0. t < d"
by (auto intro!: order_tendstoD ‹0 < d›)
then have evr: "∀⇩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 "∀⇩F t in at_left 0. t > -d"
by (auto intro!: order_tendstoD ‹0 < d›)
then have evl: "∀⇩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 "∀⇩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: "(∀⇩F t in at_left 0. flow0 rp t ∈ ball rp e)"
and evr2: "(∀⇩F t in at_right 0. flow0 rp t ∈ ball rp e)"
unfolding eventually_at_split by auto
have evl3: "(∀⇩F t in at_left 0. t > -d)"
and evr3: "(∀⇩F t in at_right 0. t < d)"
by (auto intro!: order_tendstoD ‹0 < d›)
have evl4: "(∀⇩F t in at_left 0. t < 0)"
and evr4: "(∀⇩F t in at_right 0. t > 0)"
by (auto simp: eventually_at_filter)
from evl evl2 evl3 evl4
have "∀⇩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 "∀⇩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<--<b}" using rpi subr by auto
then have rpr1:"flow0 rp (dr) ∈ r1" unfolding r1_def using ‹d > dr› ‹dr > 0›
by auto
have "rp ∈ {a<--<flow0 x t2}" using rpi subl by auto
then have rpr2:"flow0 rp (dl) ∈ 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<..<d}) ⊆ 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, opaque_lifting) closed_segment_commute ends_in_segment(1) local.existence_ivl_trans' local.flow_undefined0 real_Icc_closed_segment subset_eq ‹t1 ≤ t2›)
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..<T}. flow0 (flow0 x (t2 + dr)) s ∈ 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
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<--<flow0 x t2}"
using ‹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<..<d}) ⊆ 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, opaque_lifting) closed_segment_commute ends_in_segment(1) local.existence_ivl_trans' local.flow_undefined0 real_Icc_closed_segment subset_eq ‹t1 ≤ t2›)
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..<T}. flow0 (flow0 x (t2 + dr)) s ∈ 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
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<--<flow0 x t2}"
using ‹t > t2› ‹t ∈ existence_ivl0 x› inner outer by blast
}
ultimately show
"flow0 x t ∉ {a<--<flow0 x t2}" by auto
qed
lemma open_segment_trichotomy:
fixes x y a b::'a
assumes x:"x ∈ {a<--<b}"
assumes y:"y ∈ {a<--<b}"
shows "x = y ∨ y ∈ {x<--<b} ∨ y ∈ {a<--<x}"
proof -
from Un_open_segment[OF y]
have "{a<--<y} ∪ {y} ∪ {y<--<b} = {a<--<b}" .
then have "x ∈ {a<--<y} ∨ x = y ∨ x ∈ {y <--<b}" using x by blast
moreover {
assume "x ∈ {a<--<y}"
then have "y ∈ {x<--<b}" using open_segment_subsegment
using open_segment_commute y by blast
}
moreover {
assume "x ∈ {y<--<b}"
from open_segment_subsegment[OF y this]
have "y ∈ {a<--<x}" .
}
ultimately show ?thesis by blast
qed
sublocale rev: c1_on_open_R2 "-f" "-f'" rewrites "-(-f) = f" and "-(-f') = f'"
by unfold_locales (auto simp: dim2)
lemma rev_transversal_segment: "rev.transversal_segment a b = transversal_segment a b"
by (auto simp: transversal_segment_def rev.transversal_segment_def)
lemma flow0_transversal_segment_monotone_step_reverse:
assumes "transversal_segment a b"
assumes "t1 ≤ t2"
assumes "{t1..t2} ⊆ existence_ivl0 x"
assumes x1: "flow0 x t1 ∈ {a<--<b}"
assumes x2: "flow0 x t2 ∈ {a<--<flow0 x t1}"
assumes "⋀t. t ∈ {t1<..<t2} ⟹ flow0 x t ∉ {a<--<b}"
assumes "t < t1" "t ∈ existence_ivl0 x"
shows "flow0 x t ∉ {a<--<flow0 x t1}"
proof -
note exist = ‹{t1..t2} ⊆ existence_ivl0 x›
note t1t2 = ‹⋀t. t ∈ {t1<..<t2} ⟹ flow0 x t ∉ {a<--<b}›
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<--<b}"
and x1_mem: "flow0 x t1 ∈ {flow0 x t2<--<b}"
using i1 i2
by (auto simp: line_in_subsegment line_line1)
have transversal': "rev.transversal_segment a b"
using ‹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<--<rev.flow0 (flow0 x t2) (t2 - t1)}"
apply (rule rev.flow0_transversal_segment_monotone_step[OF transversal' time' exivl'])
using exist ‹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<--<b}"
assumes t2: "flow0 x t2 ∈ {flow0 x t1<--<b}"
assumes t1t2: "⋀t. t ∈ {t1<..<t2} ⟹ flow0 x t ∉ {a<--<b}"
assumes t: "t < t1" "t ∈ existence_ivl0 x"
shows "flow0 x t ∉ {flow0 x t1<--<b}"
using flow0_transversal_segment_monotone_step_reverse[of b a, OF _ time exist, of t]
assms
by (auto simp: open_segment_commute transversal_segment_commute)
lemma flow0_transversal_segment_monotone_step2:
assumes transversal: "transversal_segment a b"
assumes time: "t1 ≤ t2"
assumes exist: "{t1..t2} ⊆ existence_ivl0 x"
assumes t1: "flow0 x t1 ∈ {a<--<b}"
assumes t2: "flow0 x t2 ∈ {a<--<flow0 x t1}"
assumes t1t2: "⋀t. t ∈ {t1<..<t2} ⟹ flow0 x t ∉ {a<--<b}"
shows "⋀t. t > t2 ⟹ t ∈ existence_ivl0 x ⟹ flow0 x t ∉ {flow0 x t2<--<b}"
using flow0_transversal_segment_monotone_step[of b a, OF _ time exist]
assms
by (auto simp: transversal_segment_commute open_segment_commute)
lemma flow0_transversal_segment_monotone:
assumes "transversal_segment a b"
assumes "t1 ≤ t2"
assumes "{t1..t2} ⊆ existence_ivl0 x"
assumes x1: "flow0 x t1 ∈ {a<--<b}"
assumes x2: "flow0 x t2 ∈ {flow0 x t1<--<b}"
assumes "t > t2" "t ∈ existence_ivl0 x"
shows "flow0 x t ∉ {a<--<flow0 x t2}"
proof -
note exist = ‹{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<--<b}"
using i1 i2
by simp
let ?T = "{s ∈ {t1..t2}. flow0 x s ∈ {a--b}}"
let ?T' = "{s ∈ {t1..<t2}. flow0 x s ∈ {a<--<b}}"
from flow_transversal_segment_finite_intersections[OF ‹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<--<b}"
using ‹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<--<b}" if "t ∈ {tm<..<t2}" for t
using ‹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<--<b}" |
"flow0 x t2 ∈ {a<--<flow0 x tm}" |
"flow0 x tm = flow0 x t2"
by blast
then show "flow0 x t ∉ {a<--<flow0 x t2}"
proof cases
case 1
from flow0_transversal_segment_monotone_step[OF ‹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<--<flow0 x tm}" by auto
then have False
using x1 x2 2 i1 i2
apply (auto simp: line_in_subsegment line_in_subsegment2)
by (smt greaterThanLessThan_iff in_open_segment_iff_line line_in_subsegment2 tm_in)
then show ?thesis by simp
next
case 3
have "t1 ≠ 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<..<t2})"
using ‹tm ≤ t2› 3
apply auto
by (smt greaterThanLessThan_iff image_eqI)
finally have "flow0 x t1 ∈ flow0 x ` (insert t2 {tm<..<t2})"
by auto
then have "flow0 x t1 ∈ flow0 x ` {tm<..<t2}" using x1neqx2
by auto
moreover have "… ∩ {a<--<b} = {}"
using tm_exclude
by auto
ultimately have False using x1 by auto
then show ?thesis by blast
qed
qed
subsection ‹Straightening›
text ‹ This lemma uses the implicit function theorem ›
lemma cross_time_continuous:
assumes "transversal_segment a b"
assumes "x ∈ {a<--<b}"
assumes "e > 0"
obtains d t where "d > 0" "continuous_on (ball x d) t"
"⋀y. y ∈ ball x d ⟹ flow0 y (t y) ∈ {a<--<b}"
"⋀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)) /⇩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 "∀⇩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<--<b}›
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 "∀⇩F y in at x. flow0 y (t y) ∈ ?S" .
ultimately
have "∀⇩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<--<b}"
by (auto simp add: in_open_segment_iff_rot ‹a ≠ b›) (auto simp: s_def e2_def in_segment)
then have "⋀y. y ∈ ball x d ⟹ flow0 y (t y) ∈ {a<--<b}"
apply (rule set_mp)
using d1 d2 ‹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<--<b}"
obtains s where
"s ⇢⇘⇙ ∞"
"(flow0 x ∘ s) ⇢ p"
"∀⇩F n in sequentially. flow0 x (s n) ∈ {a<--<b} ∧ 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 ⇢⇘⇙ ∞" "(flow0 x ∘ t) ⇢ p"
by (auto simp: ω_limit_point_def)
note t = ‹t ⇢⇘⇙ ∞› ‹(flow0 x ∘ t) ⇢ p›
note [tendsto_intros] = t(2)
from cross_time_continuous[OF assms(1,4) zero_less_one]
obtain τ δ
where "0 < δ" "continuous_on (ball p δ) τ"
"τ p = 0" "(⋀y. y ∈ ball p δ ⟹ ¦τ y¦ < 1)"
"(⋀y. y ∈ ball p δ ⟹ flow0 y (τ y) ∈ {a<--<b})"
by metis
note τ =
‹(⋀y. y ∈ ball p δ ⟹ flow0 y (τ y) ∈ {a<--<b})›
‹(⋀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: "∀⇩F n in at_top. flow0 x (t n) ∈ ball p δ"
apply simp
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 "∀⇩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: "∀⇩F n in sequentially. t n > 1"
using filterlim_at_top_dense t(1) by auto
then have ev_eq: "∀⇩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 "∀⇩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
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 "∀⇩F n in sequentially. flow0 x (s n) ∈ {a<--<b}"
using ev_eq ev_in_ball
apply eventually_elim
apply (drule sym)
apply simp
apply (rule τ) by simp
moreover have "∀⇩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 "∀⇩F n in sequentially. flow0 x (s n) ∈ {a<--<b} ∧ s n ∈ existence_ivl0 x"
by eventually_elim auto
}
ultimately show ?thesis ..
qed
lemma filterlim_at_top_tendstoE:
assumes "e > 0"
assumes "filterlim s at_top sequentially"
assumes "(flow0 x ∘ s) ⇢ u"
assumes "∀⇩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 "∀⇩F n in sequentially. b < s n"
by (simp add: filterlim_at_top_dense)
moreover have "∀⇩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 "∀⇩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<--<b}"
by (smt dist_commute dist_in_open_segment open_segment_subsegment v x(1))
moreover have "v ∈ {a<--<b}" using v
by (metis ends_in_segment(1) segment_open_subset_closed subset_eq subset_segment(4) u)
ultimately show ?thesis using open_segment_trichotomy[OF _ x(2)]
by blast
qed
lemma open_segment_separate_right:
fixes u v x a b::'a
assumes u:"u ∈ {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<--<v}"
by (smt dist_commute dist_in_open_segment open_segment_commute open_segment_subsegment v x(1))
moreover have "v ∈ {a<--<b}" using v
by (metis ends_in_segment(1) segment_open_subset_closed subset_eq subset_segment(4) u)
ultimately show ?thesis using open_segment_trichotomy[OF _ x(2)]
by blast
qed
lemma no_two_ω_limit_points:
assumes transversal: "transversal_segment a b"
assumes ex_pos: "{0..} ⊆ existence_ivl0 x"
assumes u: "ω_limit_point x u" "u ∈ {a<--<b}"
assumes v: "ω_limit_point x v" "v ∈ {a<--<b}"
assumes uv: "v ∈ {u<--<b}"
shows False
proof -
have unotv: "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"
"∀⇩F n in sequentially. flow0 x (su n) ∈ {a<--<b} ∧ 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"
"∀⇩F n in sequentially. flow0 x (sv n) ∈ {a<--<b} ∧ 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<--<b}"
"su1 ∈ 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<--<b}"
"su2 ∈ 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<--<b}"
"su3 ∈ 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)
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<--<v}" .
have "dist (flow0 x su2) v < dist v (flow0 x su1)" using d1
by (smt dist_commute duv_def su2(4))
from open_segment_separate_right[OF v(2) su1l this su2(2)]
have su2l:"flow0 x su2 ∈ {flow0 x su1<--<b}" .
then have su2ll:"flow0 x su2 ∈ {u<--<b}"
by (smt dist_commute dist_pos_lt duv_def open_segment_subsegment pos_half_less open_segment_separate_right su2(2) su2(4) u(2) uv v(2) unotv)
have "dist (flow0 x su2) 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<--<flow0 x su2}" .
from flow0_transversal_segment_monotone[OF transversal * su1(2) su2l su3(1) su3(3)]
have "flow0 x su3 ∉ {a <--<flow0 x su2}" .
thus False using su3l by auto
qed
subsection ‹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<--<b}"
shows "ω_limit_set x ∩ {a<--<b} = {u}"
proof (rule ccontr)
assume "ω_limit_set x ∩ {a<--<b} ≠ {u}"
then
obtain v where uv: "u ≠ v"
and v: "ω_limit_point x v" "v ∈ {a<--<b}" using assms unfolding ω_limit_set_def
by fastforce
have u:"ω_limit_point x u" "u ∈ {a<--<b}" using assms unfolding ω_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)"
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
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<--<b}" by blast
then have "l ∈ ω_limit_set x ∩ {a<--<b}" using lr by auto
from unique_transversal_segment_intersection[OF ab(1) ex_pos this]
have luniq: "ω_limit_set x ∩ {a<--<b} = {l} " .
from cross_time_continuous[OF ab, of 1]
obtain d t where dt: "0 < d"
"(⋀y. y ∈ ball l d ⟹ flow0 y (t y) ∈ {a<--<b})"
"(⋀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<--<b}" using dt by auto
moreover have sr: "(s ∘ 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<--<b}" by auto
from unique_transversal_segment_intersection[OF ab(1) ex_pos this]
have "flow0 ((s ∘ 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<--<b}"
obtains s where
"s ⇢⇘⇙ -∞"
"(flow0 x ∘ s) ⇢ p"
"∀⇩F n in sequentially.
flow0 x (s n) ∈ {a<--<b} ∧
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"
"∀⇩F n in sequentially. flow0 x (- s n) ∈ {a<--<b} ∧ s n ∈ uminus ` existence_ivl0 x" .
then have "filterlim (-s) at_bot sequentially"
"(flow0 x ∘ (-s)) ⇢ p"
"∀⇩F n in sequentially. flow0 x ((-s) n) ∈ {a<--<b} ∧ (-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<--<b}" by blast
from zy
obtain t1 t2 where t1: "flow0 y t1 ∈ {a<--<b}" and t2: "flow0 y t2 ∈ {a<--<b}" and "t1 ≠ 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"
"∀⇩F n in sequentially. flow0 y (s n) ∈ {a<--<b}"
by auto
from eventually_happens[OF this(3)] obtain t1 where t1: "flow0 y t1 ∈ {a<--<b}" by auto
have "∀⇩F n in sequentially. s n > t1"
using filterlim_at_top_dense s(1) by auto
with s(3) have "∀⇩F n in sequentially. flow0 y (s n) ∈ {a<--<b} ∧ s n > t1"
by eventually_elim simp
from eventually_happens[OF this] obtain t2 where t2: "flow0 y t2 ∈ {a<--<b}" and "t1 ≠ 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"
"∀⇩F n in sequentially. flow0 y (s n) ∈ {a<--<b}"
by auto
from eventually_happens[OF this(3)] obtain t1 where t1: "flow0 y t1 ∈ {a<--<b}" by auto
have "∀⇩F n in sequentially. s n < t1"
using filterlim_at_bot_dense s(1) by auto
with s(3) have "∀⇩F n in sequentially. flow0 y (s n) ∈ {a<--<b} ∧ s n < t1"
by eventually_elim simp
from eventually_happens[OF this] obtain t2 where t2: "flow0 y t2 ∈ {a<--<b}" and "t1 ≠ t2"
by auto
from t1 this show ?thesis ..
qed
have "flow0 y t1 ∈ ω_limit_set x ∩ {a<--<b}" using t1 UNIV_I yinv by auto
moreover have "flow0 y t2 ∈ ω_limit_set x ∩ {a<--<b}" using t2 UNIV_I yinv by auto
ultimately have feq:"flow0 y t1 = flow0 y t2"
using unique_transversal_segment_intersection[OF ‹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
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
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
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
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