# Theory Analysis_Misc

section ‹Additions to HOL-Analysis›
theory Analysis_Misc
imports
Ordinary_Differential_Equations.ODE_Analysis
begin

subsection ‹Unsorted Lemmas (TODO: sort!)›

lemma uminus_uminus_image: "uminus  uminus  S = S"
by (auto simp: image_image)

lemma in_uminus_image_iff[simp]: "x ∈ uminus  S ⟷ - x ∈ S"
by force

lemma closed_subsegmentI:
"w + t *⇩R (z - w) ∈ {x--y}"
if "w ∈ {x -- y}" "z ∈ {x -- y}" and t: "0 ≤ t" "t≤ 1"
proof -
from that obtain u v where
w_def: "w = (1 - u) *⇩R x + u *⇩R y" and u: "0 ≤ u" "u ≤ 1"
and z_def: "z = (1 - v) *⇩R x + v *⇩R y" and v: "0 ≤ v" "v ≤ 1"
by (auto simp: in_segment)
have "w + t *⇩R (z - w) =
(1 - (u - t * (u - v))) *⇩R x + (u - t * (u - v)) *⇩R y"
by (simp add: algebra_simps w_def z_def)
also have "… ∈ {x -- y}"
unfolding closed_segment_image_interval
apply (rule imageI)
using t u v
apply auto
apply (metis (full_types) diff_0_right diff_left_mono linear mult_left_le_one_le mult_nonneg_nonpos order.trans)
by (smt mult_left_le_one_le mult_nonneg_nonneg vector_space_over_itself.scale_right_diff_distrib)
finally show ?thesis .
qed

lemma tendsto_minus_cancel_right: "((λx. -g x) ⤏ l) F ⟷ (g ⤏ -l) F"
― ‹cf @{thm tendsto_minus_cancel_left}›

lemma tendsto_nhds_continuousI: "(f ⤏ l) (nhds x)" if "(f ⤏ l) (at x)" "f x = l"
― ‹TODO: the assumption is continuity of f at x›
proof (rule topological_tendstoI)
fix S::"'b set" assume "open S" "l ∈ S"
from topological_tendstoD[OF that(1) this]
have "∀⇩F x in at x. f x ∈ S" .
then show "∀⇩F x in nhds x. f x ∈ S"
unfolding eventually_at_filter
by eventually_elim (auto simp: that ‹l ∈ S›)
qed

lemma inj_composeD:
assumes "inj (λx. g (t x))"
shows "inj t"
using assms
by (auto simp: inj_def)

lemma compact_sequentialE:
fixes S T::"'a::first_countable_topology set"
assumes "compact S"
assumes "infinite T"
assumes "T ⊆ S"
obtains t::"nat ⇒ 'a" and l::'a
where "⋀n. t n ∈ T" "⋀n. t n ≠ l" "t ⇢ l" "l ∈ S"
proof -
from Heine_Borel_imp_Bolzano_Weierstrass[OF assms]
obtain l where "l ∈ S" "l islimpt T" by metis
then obtain t where "t n ∈ T" "t n ≠ l" "t ⇢ l" "l ∈ S" for n unfolding islimpt_sequential
by auto
then show ?thesis ..
qed

lemma infinite_countable_subsetE:
fixes S::"'a set"
assumes "infinite S"
obtains g::"nat⇒'a" where "inj g" "range g ⊆ S"
using assms

lemma real_quad_ge: "2 * (an * bn) ≤ an * an + bn * bn" for an bn::real
by (sos "(((A<0 * R<1) + (R<1 * (R<1 * [an + ~1*bn]^2))))")

lemma inner_quad_ge: "2 * (a ∙ b) ≤ a ∙ a + b ∙ b"
for a b::"'a::euclidean_space"― ‹generalize?›
proof -
show ?thesis
by (subst (1 2 3) euclidean_inner)
qed

lemma inner_quad_gt: "2 * (a ∙ b) < a ∙ a + b ∙ b"
if "a ≠ b"
for a b::"'a::euclidean_space"― ‹generalize?›
proof -
from that obtain i where "i ∈ Basis" "a ∙ i ≠ b ∙ i"
by (auto simp: euclidean_eq_iff[where 'a='a])
then have "2 * (a ∙ i * (b ∙ i)) < a ∙ i * (a ∙ i) + b ∙ i * (b ∙ i)"
using sum_sqs_eq[of "a∙i" "b∙i"]
then show ?thesis
by (subst (1 2 3) euclidean_inner)
(auto simp add: ‹i ∈ Basis› sum.distrib[symmetric] sum_distrib_left
qed

lemma closed_segment_line_hyperplanes:
"{a -- b} = range (λu. a + u *⇩R (b - a)) ∩ {x. a ∙ (b - a) ≤ x ∙ (b - a) ∧ x ∙ (b - a) ≤ b ∙ (b - a)}"
if "a ≠ b"
for a b::"'a::euclidean_space"
proof safe
fix x assume x: "x ∈ {a--b}"
then obtain u where u: "0 ≤ u" "u ≤ 1" and x_eq: "x = a + u *⇩R (b - a)"
by (auto simp add: in_segment algebra_simps)
show "x ∈ range (λu. a + u *⇩R (b - a))" using x_eq by auto
have "2 * (a ∙ b) ≤ a ∙ a + b ∙ b"
then have "u * (2 * (a ∙ b) - a ∙ a - b ∙ b) ≤ 0"
"0 ≤ (1 - u) * (a ∙ a + b ∙ b - a ∙ b * 2)"
then show " a ∙ (b - a) ≤ x ∙ (b - a)" "x ∙ (b - a) ≤ b ∙ (b - a)"
by (auto simp: x_eq algebra_simps power2_eq_square inner_commute)
next
fix u assume
"a ∙ (b - a) ≤ (a + u *⇩R (b - a)) ∙ (b - a)"
"(a + u *⇩R (b - a)) ∙ (b - a) ≤ b ∙ (b - a)"
then have "0 ≤ u * ((b - a) ∙ (b - a))" "0 ≤ (1 - u) * ((b - a) ∙ (b - a))"
by (auto simp: algebra_simps)
then have "0 ≤ u" "u ≤ 1"
using inner_ge_zero[of "(b - a)"] that
then show "a + u *⇩R (b - a) ∈ {a--b}"
by (auto simp: in_segment algebra_simps)
qed

lemma open_segment_line_hyperplanes:
"{a <--< b} = range (λu. a + u *⇩R (b - a)) ∩ {x. a ∙ (b - a) < x ∙ (b - a) ∧ x ∙ (b - a) < b ∙ (b - a)}"
if "a ≠ b"
for a b::"'a::euclidean_space"
proof safe
fix x assume x: "x ∈ {a<--<b}"
then obtain u where u: "0 < u" "u < 1" and x_eq: "x = a + u *⇩R (b - a)"
by (auto simp add: in_segment algebra_simps)
show "x ∈ range (λu. a + u *⇩R (b - a))" using x_eq by auto
have "2 * (a ∙ b) < a ∙ a + b ∙ b" using that
then have "u * (2 * (a ∙ b) - a ∙ a - b ∙ b) < 0"
"0 < (1 - u) * (a ∙ a + b ∙ b - a ∙ b * 2)"
then show " a ∙ (b - a) < x ∙ (b - a)" "x ∙ (b - a) < b ∙ (b - a)"
by (auto simp: x_eq algebra_simps power2_eq_square inner_commute)
next
fix u assume
"a ∙ (b - a) < (a + u *⇩R (b - a)) ∙ (b - a)"
"(a + u *⇩R (b - a)) ∙ (b - a) < b ∙ (b - a)"
then have "0 < u * ((b - a) ∙ (b - a))" "0 < (1 - u) * ((b - a) ∙ (b - a))"
by (auto simp: algebra_simps)
then have "0 < u" "u < 1"
using inner_ge_zero[of "(b - a)"] that
then show "a + u *⇩R (b - a) ∈ {a<--<b}"
by (auto simp: in_segment algebra_simps that)
qed

lemma at_within_interior: "NO_MATCH UNIV S ⟹ x ∈ interior S ⟹ at x within S = at x"
by (auto intro: at_within_interior)

lemma tendsto_at_topI:
"(f ⤏ l) at_top" if "⋀e. 0 < e ⟹ ∃x0. ∀x≥x0. dist (f x) l < e"
for f::"'a::linorder_topology ⇒ 'b::metric_space"
using that
apply (intro tendstoI)
unfolding eventually_at_top_linorder
by auto

lemma tendsto_at_topE:
fixes f::"'a::linorder_topology ⇒ 'b::metric_space"
assumes "(f ⤏ l) at_top"
assumes "e > 0"
obtains x0 where "⋀x. x ≥ x0 ⟹ dist (f x) l < e"
proof -
from assms(1)[THEN tendstoD, OF assms(2)]
have "∀⇩F x in at_top. dist (f x) l < e" .
then show ?thesis
unfolding eventually_at_top_linorder
by (auto intro: that)
qed
lemma tendsto_at_top_iff: "(f ⤏ l) at_top ⟷ (∀e>0. ∃x0. ∀x≥x0. dist (f x) l < e)"
for f::"'a::linorder_topology ⇒ 'b::metric_space"
by (auto intro!: tendsto_at_topI elim!: tendsto_at_topE)

lemma tendsto_at_top_eq_left:
fixes f g::"'a::linorder_topology ⇒ 'b::metric_space"
assumes "(f ⤏ l) at_top"
assumes "⋀x. x ≥ x0 ⟹ f x = g x"
shows "(g ⤏ l) at_top"
unfolding tendsto_at_top_iff
by (metis (no_types, hide_lams) assms(1) assms(2) linear order_trans tendsto_at_topE)

lemma lim_divide_n: "(λx. e / real x) ⇢ 0"
proof -
have "(λx. e * inverse (real x)) ⇢ 0"
by (auto intro: tendsto_eq_intros lim_inverse_n)
then show ?thesis by (simp add: inverse_eq_divide)
qed

definition at_top_within :: "('a::order) set ⇒ 'a filter"
where "at_top_within s = (INF k ∈ s. principal ({k ..} ∩ s)) "

lemma at_top_within_at_top[simp]:
shows "at_top_within UNIV = at_top"
unfolding at_top_within_def at_top_def
by (auto)

lemma at_top_within_empty[simp]:
shows "at_top_within {} = top"
unfolding at_top_within_def
by (auto)

definition "nhds_set X = (INF S∈{S. open S ∧ X ⊆ S}. principal S)"

lemma eventually_nhds_set:
"(∀⇩F x in nhds_set X. P x) ⟷ (∃S. open S ∧ X ⊆ S ∧ (∀x∈S. P x))"
unfolding nhds_set_def by (subst eventually_INF_base) (auto simp: eventually_principal)

term "filterlim f (nhds_set (frontier X)) F" ― ‹f tends to the boundary of X?›

text ‹somewhat inspired by @{thm islimpt_range_imp_convergent_subsequence} and its dependencies.
The class constraints seem somewhat arbitrary, perhaps this can be generalized in some way.
›
lemma limpt_closed_imp_exploding_subsequence:―‹TODO: improve name?!›
fixes f::"'a::{heine_borel,real_normed_vector} ⇒ 'b::{first_countable_topology, t2_space}"
assumes cont[THEN continuous_on_compose2, continuous_intros]: "continuous_on T f"
assumes closed: "closed T"
assumes bound: "⋀t. t ∈ T ⟹ f t ≠ l"
assumes limpt: "l islimpt (f  T)"
obtains s where
"(f ∘ s) ⇢ l"
"⋀i. s i ∈ T"
"⋀C. compact C ⟹ C ⊆ T ⟹ ∀⇩F i in sequentially. s i ∉ C"
proof -
from countable_basis_at_decseq[of l]
obtain A where A: "⋀i. open (A i)" "⋀i. l ∈ A i"
and evA: "⋀S. open S ⟹ l ∈ S ⟹ eventually (λi. A i ⊆ S) sequentially"
by blast

from closed_Union_compact_subsets[OF closed]
obtain C
where C: "(⋀n. compact (C n))" "(⋀n. C n ⊆ T)" "(⋀n. C n ⊆ C (Suc n))" "⋃ (range C) = T"
and evC: "(⋀K. compact K ⟹ K ⊆ T ⟹ ∀⇩F i in sequentially. K ⊆ C i)"
by (metis eventually_sequentially)

have AC: "l ∈ A i - f  C i" "open (A i - f  C i)" for i
using C bound
by (fastforce intro!: open_Diff A compact_imp_closed compact_continuous_image continuous_intros)+

from islimptE[OF limpt AC] have "∃t∈T. f t ∈ A i - f  C i ∧ f t ≠ l" for i by blast
then obtain t where t: "⋀i. t i ∈ T" "⋀i. f (t i) ∈ A i - f  C i" "⋀i. f (t i) ≠ l"
by metis

have "(f o t) ⇢ l"
using t
by (auto intro!: topological_tendstoI dest!: evA elim!: eventually_mono)
moreover
have "⋀i. t i ∈ T" by fact
moreover
have "∀⇩F i in sequentially. t i ∉ K" if "compact K" "K ⊆ T" for K
using evC[OF that]
by eventually_elim (use t in auto)
ultimately show ?thesis ..
qed

lemma Inf_islimpt: "bdd_below S ⟹ Inf S ∉ S ⟹ S ≠ {} ⟹ Inf S islimpt S" for S::"real set"
by (auto simp: islimpt_in_closure intro!: closure_contains_Inf)

context linorder
begin

text ‹HOL-analysis doesn't seem to have these, maybe they were never needed.
Some variants are around @{thm Int_atLeastAtMost}, but with old-style naming conventions.
Change to the "modern" I.. convention there?›

lemma Int_Ico[simp]:
shows "{a..} ∩ {b..} = {max a b ..}"
by (auto)

lemma Int_Ici_Ico[simp]:
shows "{a..} ∩ {b..<c} = {max a b ..<c}"
by auto

lemma Int_Ico_Ici[simp]:
shows "{a..<c} ∩ {b..} = {max a b ..<c}"
by auto

lemma subset_Ico_iff[simp]:
"{a..<b} ⊆ {c..<b} ⟷ b ≤ a ∨ c ≤ a"
unfolding atLeastLessThan_def
by auto

lemma Ico_subset_Ioo_iff[simp]:
"{a..<b} ⊆ {c<..<b} ⟷ b ≤ a ∨ c < a"
unfolding greaterThanLessThan_def atLeastLessThan_def
by auto

lemma Icc_Un_Ici[simp]:
shows "{a..b} ∪ {b..} = {min a b..}"
unfolding atLeastAtMost_def atLeast_def atMost_def min_def
by auto

end

lemma at_top_within_at_top_unbounded_right:
fixes a::"'a::linorder"
shows "at_top_within {a..} = at_top"
unfolding at_top_within_def at_top_def
apply (auto intro!: INF_eq)
by (metis linorder_class.linear linorder_class.max.cobounded1 linorder_class.max.idem ord_class.atLeast_iff)

lemma at_top_within_at_top_unbounded_rightI:
fixes a::"'a::linorder"
assumes "{a..} ⊆ s"
shows "at_top_within s = at_top"
unfolding at_top_within_def at_top_def
apply (auto intro!: INF_eq)
apply (meson Ici_subset_Ioi_iff Ioi_le_Ico assms dual_order.refl dual_order.trans leI)
by (metis assms atLeast_iff atLeast_subset_iff inf.cobounded1 linear subsetD)

lemma at_top_within_at_top_bounded_right:
fixes a b::"'a::{dense_order,linorder_topology}"
assumes "a < b"
shows "at_top_within {a..<b} = at_left b"
unfolding at_top_within_def at_left_eq[OF assms(1)]
apply (auto intro!: INF_eq)
apply (smt atLeastLessThan_iff greaterThanLessThan_iff le_less lessThan_iff max.absorb1 subset_eq)
by (metis assms atLeastLessThan_iff dense linear max.absorb1 not_less order_trans)

lemma at_top_within_at_top_bounded_right':
fixes a b::"'a::{dense_order,linorder_topology}"
assumes "a < b"
shows "at_top_within {..<b} = at_left b"
unfolding at_top_within_def at_left_eq[OF assms(1)]
apply (auto intro!: INF_eq)
apply (meson atLeast_iff greaterThanLessThan_iff le_less lessThan_iff subset_eq)
by (metis Ico_subset_Ioo_iff atLeastLessThan_def dense lessThan_iff)

lemma eventually_at_top_within_linorder:
assumes sn:"s ≠ {}"
shows "eventually P (at_top_within s) ⟷ (∃x0::'a::{linorder_topology} ∈ s. ∀x ≥ x0. x∈ s ⟶ P x)"
unfolding at_top_within_def
apply (subst eventually_INF_base)
apply (auto simp:eventually_principal sn)
by (metis atLeast_subset_iff inf.coboundedI2 inf_commute linear)

lemma tendsto_at_top_withinI:
fixes f::"'a::linorder_topology ⇒ 'b::metric_space"
assumes "s ≠ {}"
assumes "⋀e. 0 < e ⟹ ∃x0 ∈ s. ∀x ∈ {x0..} ∩ s. dist (f x) l < e"
shows  "(f ⤏ l) (at_top_within s)"
apply(intro tendstoI)
unfolding at_top_within_def apply (subst eventually_INF_base)
apply (auto simp:eventually_principal assms)
by (metis atLeast_subset_iff inf.coboundedI2 inf_commute linear)

lemma tendsto_at_top_withinE:
fixes f::"'a::linorder_topology ⇒ 'b::metric_space"
assumes "s ≠ {}"
assumes "(f ⤏ l) (at_top_within s)"
assumes "e > 0"
obtains x0 where "x0 ∈ s" "⋀x. x ∈ {x0..} ∩ s ⟹ dist (f x) l < e"
proof -
from assms(2)[THEN tendstoD, OF assms(3)]
have "∀⇩F x in at_top_within s. dist (f x) l < e" .
then show ?thesis unfolding eventually_at_top_within_linorder[OF ‹s ≠ {}›]
by (auto intro: that)
qed

lemma tendsto_at_top_within_iff:
fixes f::"'a::linorder_topology ⇒ 'b::metric_space"
assumes "s ≠ {}"
shows "(f ⤏ l) (at_top_within s) ⟷ (∀e>0. ∃x0 ∈ s. ∀x ∈ {x0..} ∩ s. dist (f x) l < e)"
by (auto intro!: tendsto_at_top_withinI[OF ‹s ≠ {}›] elim!: tendsto_at_top_withinE[OF ‹s ≠ {}›])

lemma filterlim_at_top_at_top_within_bounded_right:
fixes a b::"'a::{dense_order,linorder_topology}"
fixes f::"'a ⇒ real"
assumes "a < b"
shows "filterlim f at_top (at_top_within {..<b}) = (f ⤏ ∞) (at_left b)"
unfolding filterlim_at_top_dense
at_top_within_at_top_bounded_right'[OF assms(1)]
eventually_at_left[OF assms(1)]
tendsto_PInfty
by auto

text ‹Extract a sequence (going to infinity) bounded away from l›

lemma not_tendsto_frequentlyE:
assumes "¬((f ⤏ l) F)"
obtains S where "open S" "l ∈ S" "∃⇩F x in F. f x ∉ S"
using assms
by (auto simp: tendsto_def not_eventually)

lemma not_tendsto_frequently_metricE:
assumes "¬((f ⤏ l) F)"
obtains e where "e > 0" "∃⇩F x in F. e ≤ dist (f x) l"
using assms
by (auto simp: tendsto_iff not_eventually not_less)

lemma eventually_frequently_conj: "frequently P F ⟹ eventually Q F ⟹ frequently (λx. P x ∧ Q x) F"
unfolding frequently_def
apply (erule contrapos_nn)
subgoal premises prems
using prems by eventually_elim auto
done

lemma frequently_at_top:
"(∃⇩F t in at_top. P t) ⟷ (∀t0. ∃t>t0. P t)"
for P::"'a::{linorder,no_top}⇒bool"
by (auto simp: frequently_def eventually_at_top_dense)

lemma frequently_at_topE:
fixes P::"nat ⇒ 'a::{linorder,no_top}⇒_"
assumes freq[rule_format]: "∀n. ∃⇩F a in at_top. P n a"
obtains s::"nat⇒'a"
where "⋀i. P i (s i)" "strict_mono s"
proof -
have "∃f. ∀n. P n (f n) ∧ f n < f (Suc n)"
proof (rule dependent_nat_choice)
from frequently_ex[OF freq[of 0]] show "∃x. P 0 x" .
fix x n assume "P n x"
from freq[unfolded frequently_at_top, rule_format, of x "Suc n"]
obtain y where "P (Suc n) y" "y > x" by auto
then show "∃y. P (Suc n) y ∧ x < y"
by auto
qed
then obtain s where "⋀i. P i (s i)" "strict_mono s"
unfolding strict_mono_Suc_iff by auto
then show ?thesis ..
qed

lemma frequently_at_topE':
fixes P::"nat ⇒ 'a::{linorder,no_top}⇒_"
assumes freq[rule_format]: "∀n. ∃⇩F a in at_top. P n a"
and g: "filterlim g at_top sequentially"
obtains s::"nat⇒'a"
where "⋀i. P i (s i)" "strict_mono s" "⋀n. g n ≤ s n"
proof -
have "∀n. ∃⇩F a in at_top. P n a ∧ g n ≤ a"
using freq
by (auto intro!: eventually_frequently_conj)
from frequently_at_topE[OF this] obtain s where "⋀i. P i (s i)" "strict_mono s" "⋀n. g n ≤ s n"
by metis
then show ?thesis ..
qed

lemma frequently_at_top_at_topE:
fixes P::"nat ⇒ 'a::{linorder,no_top}⇒_" and g::"nat⇒'a"
assumes "∀n. ∃⇩F a in at_top. P n a" "filterlim g at_top sequentially"
obtains s::"nat⇒'a"
where "⋀i. P i (s i)" "filterlim s at_top sequentially"
proof -
from frequently_at_topE'[OF assms]
obtain s where s: "(⋀i. P i (s i))" "strict_mono s" "(⋀n. g n ≤ s n)" by blast
have s_at_top: "filterlim s at_top sequentially"
by (rule filterlim_at_top_mono) (use assms s in auto)
with s(1) show ?thesis ..
qed

(* Extract a strict monotone and sequence converging to something other than l *)
lemma not_tendsto_convergent_seq:
fixes f::"real ⇒ 'a::metric_space"
assumes X: "compact (X::'a set)"
assumes im: "⋀x. x ≥ 0 ⟹ f x ∈ X"
assumes nl: "¬ ((f ⤏ (l::'a)) at_top)"
obtains s k where
"k ∈ X" "k ≠ l" "(f ∘ s) ⇢ k" "strict_mono s" "∀n. s n ≥ n"
proof -
from not_tendsto_frequentlyE[OF nl]
obtain S where "open S" "l ∈ S" "∃⇩F x in at_top. f x ∉ S" .
have "∀n. ∃⇩F x in at_top. f x ∉ S ∧ real n ≤ x"
apply (rule allI)
apply (rule eventually_frequently_conj)
apply fact
by (rule eventually_ge_at_top)
from frequently_at_topE[OF this]
obtain s where "⋀i. f (s i) ∉ S" and s: "strict_mono s" and s_ge: "(⋀i. real i ≤ s i)" by metis
then have "0 ≤ s i" for i using dual_order.trans of_nat_0_le_iff by blast
then have "∀n. (f ∘ s) n ∈ X" using im by auto
from X[unfolded compact_def, THEN spec, THEN mp, OF this]
obtain k r where k: "k ∈ X" and r: "strict_mono r" and kLim: "(f ∘ s ∘ r) ⇢ k" by metis
have "k ∈ X - S"
by (rule Lim_in_closed_set[of "X - S", OF _ _ _ kLim])
(auto simp: im ‹0 ≤ s _›  ‹⋀i. f (s i) ∉ S› intro!: ‹open S› X intro: compact_imp_closed)

note k
moreover have "k ≠ l" using ‹k ∈ X - S› ‹l ∈ S› by auto
moreover have "(f ∘ (s ∘ r)) ⇢ k" using kLim by (simp add: o_assoc)
moreover have "strict_mono (s ∘ r)" using s r by (rule strict_mono_o)
moreover have "∀n. (s ∘ r) n ≥ n" using s_ge r
by (metis comp_apply dual_order.trans of_nat_le_iff seq_suble)
ultimately show ?thesis ..
qed

lemma harmonic_bound:
shows "1 / 2 ^(Suc n) < 1 / real (Suc n)"
proof (induction n)
case 0
then show ?case by auto
next
case (Suc n)
then show ?case
by (smt frac_less2 of_nat_0_less_iff of_nat_less_two_power zero_less_Suc)
qed

lemma INF_bounded_imp_convergent_seq:
fixes f::"real ⇒ real"
assumes cont: "continuous_on {a..} f"
assumes bound: "⋀t. t ≥ a ⟹ f t > l"
assumes inf: "(INF t∈{a..}. f t) = l"
obtains s where
"(f ∘ s) ⇢ l"
"⋀i. s i ∈ {a..}"
"filterlim s at_top sequentially"
proof -
have bound': "t ∈ {a..} ⟹ f t ≠ l" for t using bound[of t] by auto
have limpt: "l islimpt f  {a..}"
proof -
have "Inf (f  {a..}) islimpt f  {a..}"
by (rule Inf_islimpt) (auto simp: inf intro!: bdd_belowI2[where m=l] dest: bound)
then show ?thesis by (simp add: inf)
qed
from limpt_closed_imp_exploding_subsequence[OF cont closed_atLeast bound' limpt]
obtain s where s: "(f ∘ s) ⇢ l"
"⋀i. s i ∈ {a..}"
"compact C ⟹ C ⊆ {a..} ⟹ ∀⇩F i in sequentially. s i ∉ C" for C
by metis
have "∀⇩F i in sequentially. s i ≥ n" for n
using s(3)[of "{a..n}"] s(2)
by (auto elim!: eventually_mono)
then have "filterlim s at_top sequentially"
unfolding filterlim_at_top
by auto
from s(1) s(2) this
show ?thesis ..
qed

(* Generalizes to other combinations of strict_mono and filterlim *)
lemma filterlim_at_top_strict_mono:
fixes s :: "_ ⇒ 'a::linorder"
fixes r :: "nat ⇒ _"
assumes "strict_mono s"
assumes "strict_mono r"
assumes "filterlim s at_top F"
shows "filterlim (s ∘ r) at_top F"
apply (rule filterlim_at_top_mono[OF assms(3)])
by (simp add: assms(1) assms(2) seq_suble strict_mono_leD)

lemma LIMSEQ_lb:
assumes fl: "s ⇢ (l::real)"
assumes u: "l < u"
shows "∃n0. ∀n≥n0. s n < u"
proof -
from fl have "∃no>0. ∀n≥no. dist (s n) l < u-l" unfolding LIMSEQ_iff_nz using u
by simp
thus ?thesis using dist_real_def by fastforce
qed

(* Used to sharpen a tendsto with additional information*)
lemma filterlim_at_top_choose_lower:
assumes "filterlim s at_top sequentially"
assumes "(f ∘ s) ⇢ l"
obtains t where
"filterlim t at_top sequentially"
"(f ∘ t) ⇢ l"
"∀n. t n ≥ (b::real)"
proof -
obtain k where k: "∀n ≥ k. s n ≥ b" using assms(1)
unfolding filterlim_at_top eventually_sequentially by blast
define t where "t = (λn. s (n+k))"
then have "∀n. t n ≥ b" using k by simp
have "filterlim t at_top sequentially" using assms(1)
unfolding filterlim_at_top eventually_sequentially t_def
from LIMSEQ_ignore_initial_segment[OF assms(2), of "k"]
have "(λn. (f ∘ s) (n + k)) ⇢ l" .
then have "(f ∘ t) ⇢ l" unfolding t_def o_def by simp
show ?thesis
using ‹(f ∘ t) ⇢ l› ‹∀n. b ≤ t n› ‹filterlim t at_top sequentially› that by blast
qed

lemma frequently_at_top_realE:
fixes P::"nat ⇒ real ⇒ bool"
assumes "∀n. ∃⇩F t in at_top. P n t"
obtains s::"nat⇒real"
where "⋀i. P i (s i)" "filterlim s at_top at_top"
by (metis assms frequently_at_top_at_topE[OF _ filterlim_real_sequentially])

lemma approachable_sequenceE:
fixes f::"real ⇒ 'a::metric_space"
assumes "⋀t e. 0 ≤ t ⟹ 0 < e ⟹ ∃tt≥t. dist (f tt) p < e"
obtains s where "filterlim s at_top sequentially" "(f ∘ s) ⇢ p"
proof -
have "∀n. ∃⇩F i in at_top. dist (f i) p < 1/real (Suc n)"
unfolding frequently_at_top
apply (auto )
subgoal for n m
using assms[of "max 0 (m+1)" "1/(Suc n)"]
by force
done
from frequently_at_top_realE[OF this]
obtain s where s: "⋀i. dist (f (s i)) p < 1 / real (Suc i)" "filterlim s at_top sequentially"
by metis
note this(2)
moreover
have "(f o s) ⇢ p"
proof (rule tendstoI)
fix e::real assume "e > 0"
have "∀⇩F i in sequentially. 1 / real (Suc i) < e"
apply (rule order_tendstoD[OF _ ‹0 < e›])
apply (rule real_tendsto_divide_at_top)
apply (rule tendsto_intros)
by (rule filterlim_compose[OF filterlim_real_sequentially filterlim_Suc])
then show "∀⇩F x in sequentially. dist ((f ∘ s) x) p < e"
by eventually_elim (use dual_order.strict_trans s ‹e > 0› in auto)
qed
ultimately show ?thesis ..
qed

lemma mono_inc_bdd_above_has_limit_at_topI:
fixes f::"real ⇒ real"
assumes "mono f"
assumes "⋀x. f x ≤ u"
shows "∃l. (f ⤏ l) at_top"
proof -
define l where "l = Sup (range (λn. f (real n)))"
have t:"(λn. f (real n)) ⇢ l" unfolding l_def
apply (rule LIMSEQ_incseq_SUP)
apply (meson assms(2) bdd_aboveI2)
by (meson assms(1) mono_def of_nat_mono)
from tendsto_at_topI_sequentially_real[OF assms(1) t]
have "(f ⤏ l) at_top" .
thus ?thesis by blast
qed

lemma gen_mono_inc_bdd_above_has_limit_at_topI:
fixes f::"real ⇒ real"
assumes "⋀x y. x ≥ b ⟹ x ≤ y ⟹ f x ≤ f y"
assumes "⋀x. x ≥ b ⟹ f x ≤ u"
shows "∃l. (f ⤏ l) at_top"
proof -
define ff where "ff = (λx. if x ≥ b then f x else f b)"
have m1:"mono ff" unfolding ff_def mono_def using assms(1) by simp
have m2:"⋀x. ff x ≤ u" unfolding ff_def using assms(2) by simp
from mono_inc_bdd_above_has_limit_at_topI[OF m1 m2]
obtain l where "(ff ⤏ l) at_top" by blast
thus ?thesis
by (meson ‹(ff ⤏ l) at_top› ff_def tendsto_at_top_eq_left)
qed

lemma gen_mono_dec_bdd_below_has_limit_at_topI:
fixes f::"real ⇒ real"
assumes "⋀x y. x ≥ b ⟹ x ≤ y ⟹ f x ≥ f y"
assumes "⋀x. x ≥ b ⟹ f x ≥ u"
shows "∃l. (f ⤏ l) at_top"
proof -
define ff where "ff = (λx. if x ≥ b then f x else f b)"
have m1:"mono (-ff)" unfolding ff_def mono_def using assms(1) by simp
have m2:"⋀x. (-ff) x ≤ -u" unfolding ff_def using assms(2) by simp
from mono_inc_bdd_above_has_limit_at_topI[OF m1 m2]
obtain l where "(-ff ⤏ l) at_top" by blast
then have "(ff ⤏ -l) at_top"
using tendsto_at_top_eq_left tendsto_minus_cancel_left by fastforce
thus ?thesis
by (meson ‹(ff ⤏ -l) at_top› ff_def tendsto_at_top_eq_left)
qed

lemma infdist_closed:
shows "closed ({z. infdist z S ≥ e})"

(* TODO: this is a copy of LIMSEQ_norm_0 where the sequence
is bounded above in norm by a geometric series *)
lemma LIMSEQ_norm_0_pow:
assumes "k > 0" "b > 1"
assumes  "⋀n::nat. norm (s n) ≤ k / b^n"
shows "s ⇢ 0"
proof (rule metric_LIMSEQ_I)
fix e
assume "e > (0::real)"
then have "k / e > 0" using assms(1) by auto
obtain N where N: "b^(N::nat) > k / e" using assms(2)
using real_arch_pow by blast
then have "norm (s n) < e" if "n ≥ N" for n
proof -
have "k / b^n ≤ k / b^N"
by (smt assms(1) assms(2) frac_le leD power_less_imp_less_exp that zero_less_power)
also have " ... < e" using N
by (metis ‹0 < e› assms(2) less_trans mult.commute pos_divide_less_eq zero_less_one zero_less_power)
finally show ?thesis
by (meson assms less_eq_real_def not_le order_trans)
qed
then show "∃no. ∀n≥no. dist (s n) 0 < e"
by auto
qed

lemma filterlim_apply_filtermap:
assumes g: "filterlim g G F"
shows "filterlim (λx. m (g x)) (filtermap m G) F"
by (metis filterlim_def filterlim_filtermap filtermap_mono g)

lemma eventually_at_right_field_le:
"eventually P (at_right x) ⟷ (∃b>x. ∀y>x. y ≤ b ⟶ P y)"
for x :: "'a::{linordered_field, linorder_topology}"
by (smt dense eventually_at_right_field le_less_trans less_le_not_le order.strict_trans1)

subsection ‹indexing euclidean space with natural numbers›

definition  nth_eucl :: "'a::executable_euclidean_space ⇒ nat ⇒ real" where
"nth_eucl x i = x ∙ (Basis_list ! i)"
― ‹TODO: why is that and some sort of ‹lambda_eucl› nowhere available?›
definition lambda_eucl :: "(nat ⇒ real) ⇒ 'a::executable_euclidean_space" where
"lambda_eucl (f::nat⇒real) = (∑i<DIM('a). f i *⇩R Basis_list ! i)"

lemma eucl_eq_iff: "x = y ⟷ (∀i<DIM('a). nth_eucl x i = nth_eucl y i)"
for x y::"'a::executable_euclidean_space"
apply (auto simp: nth_eucl_def euclidean_eq_iff[where 'a='a])
by (metis eucl_of_list_list_of_eucl list_of_eucl_eq_iff)

bundle eucl_notation begin
notation nth_eucl (infixl "$⇩e" 90) end bundle no_eucl_notation begin no_notation nth_eucl (infixl "$⇩e" 90)
end

unbundle eucl_notation

lemma eucl_of_list_eucl_nth:
"(eucl_of_list xs::'a) $⇩e i = xs ! i" if "length xs = DIM('a::executable_euclidean_space)" "i < DIM('a)" using that apply (auto simp: nth_eucl_def) by (metis list_of_eucl_eucl_of_list list_of_eucl_nth) lemma eucl_of_list_inner: "(eucl_of_list xs::'a) ∙ eucl_of_list ys = (∑(x,y)←zip xs ys. x * y)" if "length xs = DIM('a::executable_euclidean_space)" "length ys = DIM('a::executable_euclidean_space)" using that by (auto simp: nth_eucl_def eucl_of_list_inner_eq inner_lv_rel_def) lemma self_eq_eucl_of_list: "x = eucl_of_list (map (λi. x$⇩e i) [0..<DIM('a)])"
for x::"'a::executable_euclidean_space"
by (auto simp: eucl_eq_iff[where 'a='a] eucl_of_list_eucl_nth)

lemma inner_nth_eucl: "x ∙ y = (∑i<DIM('a). x $⇩e i * y$⇩e i)"
for x y::"'a::executable_euclidean_space"
apply (subst self_eq_eucl_of_list[where x=x])
apply (subst self_eq_eucl_of_list[where x=y])
apply (subst eucl_of_list_inner)
by (auto simp: map2_map_map atLeast_upt interv_sum_list_conv_sum_set_nat)

lemma norm_nth_eucl: "norm x = L2_set (λi. x $⇩e i) {..<DIM('a)}" for x::"'a::executable_euclidean_space" unfolding norm_eq_sqrt_inner inner_nth_eucl L2_set_def by (auto simp: power2_eq_square) lemma plus_nth_eucl: "(x + y)$⇩e i = x $⇩e i + y$⇩e i"
and minus_nth_eucl: "(x - y) $⇩e i = x$⇩e i - y $⇩e i" and uminus_nth_eucl: "(-x)$⇩e i = - x $⇩e i" and scaleR_nth_eucl: "(c *⇩R x)$⇩e i = c *⇩R (x $⇩e i)" by (auto simp: nth_eucl_def algebra_simps) lemma inf_nth_eucl: "inf x y$⇩e i = min (x $⇩e i) (y$⇩e i)"
if "i < DIM('a)"
for x::"'a::executable_euclidean_space"
by (auto simp: nth_eucl_def algebra_simps inner_Basis_inf_left that inf_min)
lemma sup_nth_eucl: "sup x y $⇩e i = max (x$⇩e i) (y $⇩e i)" if "i < DIM('a)" for x::"'a::executable_euclidean_space" by (auto simp: nth_eucl_def algebra_simps inner_Basis_sup_left that sup_max) lemma le_iff_le_nth_eucl: "x ≤ y ⟷ (∀i<DIM('a). (x$⇩e i) ≤ (y $⇩e i))" for x::"'a::executable_euclidean_space" apply (auto simp: nth_eucl_def algebra_simps eucl_le[where 'a='a]) by (meson eucl_le eucl_le_Basis_list_iff) lemma eucl_less_iff_less_nth_eucl: "eucl_less x y ⟷ (∀i<DIM('a). (x$⇩e i) < (y $⇩e i))" for x::"'a::executable_euclidean_space" apply (auto simp: nth_eucl_def algebra_simps eucl_less_def[where 'a='a]) by (metis Basis_zero eucl_eq_iff inner_not_same_Basis inner_zero_left length_Basis_list nth_Basis_list_in_Basis nth_eucl_def) lemma continuous_on_nth_eucl[continuous_intros]: "continuous_on X (λx. f x$⇩e i)"
if "continuous_on X f"
by (auto simp: nth_eucl_def intro!: continuous_intros that)

subsection ‹derivatives›

lemma eventually_at_ne[intro, simp]: "∀⇩F x in at x0. x ≠ x0"
by (auto simp: eventually_at_filter)

lemma has_vector_derivative_withinD:
fixes f::"real ⇒ 'b::euclidean_space"
assumes "(f has_vector_derivative f') (at x0 within S)"
shows "((λx. (f x - f x0) /⇩R (x - x0)) ⤏ f') (at x0 within S)"
apply (rule LIM_zero_cancel)
apply (rule tendsto_norm_zero_cancel)
apply (rule Lim_transform_eventually)
proof -
show "∀⇩F x in at x0 within S. norm ((f x - f x0 - (x - x0) *⇩R f') /⇩R norm (x - x0)) =
norm ((f x - f x0) /⇩R (x - x0) - f')"
(is "∀⇩F x in _. ?th x")
unfolding eventually_at_filter
proof (safe intro!: eventuallyI)
fix x assume x: "x ≠ x0"
then have "norm ((f x - f x0) /⇩R (x - x0) - f') = norm (sgn (x - x0) *⇩R ((f x - f x0) /⇩R (x - x0) - f'))"
by simp
also have "sgn (x - x0) *⇩R ((f x - f x0) /⇩R (x - x0) - f') = ((f x - f x0) /⇩R norm (x - x0) - (x - x0) *⇩R f' /⇩R norm (x - x0))"
by (auto simp add: algebra_simps sgn_div_norm divide_simps)
also have "… = (f x - f x0 - (x - x0) *⇩R f') /⇩R norm (x - x0)" by (simp add: algebra_simps)
finally show "?th x" ..
qed
show "((λx. norm ((f x - f x0 - (x - x0) *⇩R f') /⇩R norm (x - x0))) ⤏ 0) (at x0 within S)"
by (rule tendsto_norm_zero)
(use assms in ‹auto simp: has_vector_derivative_def has_derivative_at_within›)
qed

text ‹A ‹path_connected› set ‹S› entering both ‹T› and ‹-T›
must cross the frontier of ‹T› ›
lemma path_connected_frontier:
fixes S :: "'a::real_normed_vector set"
assumes "path_connected S"
assumes "S ∩ T ≠ {}"
assumes "S ∩ -T ≠ {}"
obtains s where "s ∈ S" "s ∈ frontier T"
proof -
obtain st where st:"st ∈ S ∩ T" using assms(2) by blast
obtain sn where sn:"sn ∈ S ∩ -T" using assms(3) by blast
obtain g where g: "path g" "path_image g ⊆ S"
"pathstart g = st" "pathfinish g = sn"
using assms(1) st sn unfolding path_connected_def by blast
have a1:"pathstart g ∈ closure T" using st g(3) closure_Un_frontier by fastforce
have a2:"pathfinish g ∉ T" using sn g(4) by auto
from exists_path_subpath_to_frontier[OF g(1) a1 a2]
obtain h where "path_image h ⊆ path_image g" "pathfinish h ∈ frontier T" by metis
thus ?thesis using g(2)
by (meson in_mono pathfinish_in_path_image that)
qed

lemma path_connected_not_frontier_subset:
fixes S :: "'a::real_normed_vector set"
assumes "path_connected S"
assumes "S ∩ T ≠ {}"
assumes "S ∩ frontier T = {}"
shows "S ⊆ T"
using path_connected_frontier assms by auto

lemma compact_attains_bounds:
fixes f::"'a::topological_space ⇒ 'b::linorder_topology"
assumes compact: "compact S"
assumes ne: "S ≠ {}"
assumes cont: "continuous_on S f"
obtains l u where "l ∈ S" "u ∈ S" "⋀x. x ∈ S ⟹ f x ∈ {f l .. f u}"
proof -
from compact_continuous_image[OF cont compact]
have compact_image: "compact (f  S)" .
have ne_image: "f  S ≠ {}" using ne by simp
from compact_attains_inf[OF compact_image ne_image]
obtain l where "l ∈ S" "⋀x. x ∈ S ⟹ f l ≤ f x" by auto
moreover
from compact_attains_sup[OF compact_image ne_image]
obtain u where "u ∈ S" "⋀x. x ∈ S ⟹ f x ≤ f u" by auto
ultimately
have "l ∈ S" "u ∈ S" "⋀x. x ∈ S ⟹ f x ∈ {f l .. f u}" by auto
then show ?thesis ..
qed

lemma uniform_limit_const[uniform_limit_intros]:
"uniform_limit S (λx y. f x) (λ_. l) F" if "(f ⤏ l) F"
apply (auto simp: uniform_limit_iff)
subgoal for e
using tendstoD[OF that(1), of e]
by (auto simp: eventually_mono)
done

subsection ‹Segments›

text ‹‹closed_segment› throws away the order that our intuition keeps›

definition line::"'a::real_vector ⇒ 'a ⇒ real ⇒ 'a"
("{_ -- _}⇘_⇙")
where "{a -- b}⇘u⇙ = a + u *⇩R (b - a)"

abbreviation "line_image a b U ≡(λu. {a -- b}⇘u⇙)  U"
notation line_image ("{_ -- _}⇘_⇙")

lemma in_closed_segment_iff_line: "x ∈ {a -- b} ⟷ (∃c∈{0..1}. x = line a b c)"
by (auto simp: in_segment line_def algebra_simps)

lemma in_open_segment_iff_line: "x ∈ {a <--< b} ⟷ (∃c∈{0<..<1}. a ≠ b ∧ x = line a b c)"
by (auto simp: in_segment line_def algebra_simps)

lemma line_convex_combination1: "(1 - u) *⇩R line a b i + u *⇩R b = line a b (i + u - i * u)"
by (auto simp: line_def algebra_simps)

lemma line_convex_combination2: "(1 - u) *⇩R a + u *⇩R line a b i = line a b (i*u)"
by (auto simp: line_def algebra_simps)

lemma line_convex_combination12: "(1 - u) *⇩R line a b i + u *⇩R line a b j = line a b (i + u * (j - i))"
by (auto simp: line_def algebra_simps)

lemma mult_less_one_less_self: "0 < x ⟹ i < 1 ⟹ i * x < x" for i x::real
by auto

lemma plus_times_le_one_lemma: "i + u - i * u ≤ 1" if "i ≤ 1" "u ≤ 1" for i u::real
by (simp add: diff_le_eq sum_le_prod1 that)

lemma plus_times_less_one_lemma: "i + u - i * u < 1" if "i < 1" "u < 1" for i u::real
proof -
have "u * (1 - i) < 1 - i"
using that by force
then show ?thesis by (simp add: algebra_simps)
qed

lemma line_eq_endpoint_iff[simp]:
"line a b i = b ⟷ (a = b ∨ i = 1)"
"a = line a b i ⟷ (a = b ∨ i = 0)"
by (auto simp: line_def algebra_simps)

lemma line_eq_iff[simp]: "line a b x = line a b y ⟷ (x = y ∨ a = b)"
by (auto simp: line_def)

lemma line_open_segment_iff:
"{line a b i<--<b} = line a b  {i<..<1}"
if "i < 1" "a ≠ b"
using that
apply (auto simp: in_segment line_convex_combination1 plus_times_less_one_lemma)
subgoal for j
apply (rule exI[where x="(j - i)/(1 - i)"])
apply (auto simp: divide_simps algebra_simps)
by (metis add_diff_cancel less_numeral_extra(4) mult_2_right plus_times_less_one_lemma that(1))
done

lemma open_segment_line_iff:
"{a<--<line a b i} = line a b  {0<..<i}"
if "0 < i" "a ≠ b"
using that
apply (auto simp: in_segment line_convex_combination2 plus_times_less_one_lemma)
subgoal for j
apply (rule exI[where x="j/i"])
by (auto simp: )
done

lemma line_closed_segment_iff:
"{line a b i--b} = line a b  {i..1}"
if "i ≤ 1" "a ≠ b"
using that
apply (auto simp: in_segment line_convex_combination1 mult_le_cancel_right2 plus_times_le_one_lemma)
subgoal for j
apply (rule exI[where x="(j - i)/(1 - i)"])
apply (auto simp: divide_simps algebra_simps)
by (metis add_diff_cancel less_numeral_extra(4) mult_2_right plus_times_less_one_lemma that(1))
done

lemma closed_segment_line_iff:
"{a--line a b i} = line a b  {0..i}"
if "0 < i" "a ≠ b"
using that
apply (auto simp: in_segment line_convex_combination2 plus_times_less_one_lemma)
subgoal for j
apply (rule exI[where x="j/i"])
by (auto simp: )
done

lemma closed_segment_line_line_iff: "{line a b i1--line a b i2} = line a b  {i1..i2}" if "i1 ≤ i2"
using that
apply (auto simp: in_segment line_convex_combination12 intro!: imageI)
apply (smt mult_left_le_one_le)
subgoal for u
by (rule exI[where x="(u - i1)/(i2-i1)"]) auto
done

lemma line_line1: "line (line a b c) b x = line a b (c + x - c * x)"

lemma line_line2: "line a (line a b c) x = line a b (c*x)"

lemma line_in_subsegment:
"i1 < 1 ⟹ i2 < 1 ⟹ a ≠ b ⟹ line a b i1 ∈ {line a b i2<--<b} ⟷ i2 < i1"
by (auto simp: line_open_segment_iff intro!: imageI)

lemma line_in_subsegment2:
"0 < i2 ⟹ 0 < i1 ⟹ a ≠ b ⟹ line a b i1 ∈ {a<--<line a b i2} ⟷ i1 < i2"
by (auto simp: open_segment_line_iff intro!: imageI)

lemma line_in_open_segment_iff[simp]:
"line a b i ∈ {a<--<b} ⟷ (a ≠ b ∧ 0 < i ∧ i < 1)"
by (auto simp: in_open_segment_iff_line)

subsection ‹Open Segments›

lemma open_segment_subsegment:
assumes "x1 ∈ {x0<--<x3}"
"x2 ∈ {x1<--<x3}"
shows "x1 ∈ {x0<--<x2}"
using assms
proof -― ‹TODO: use ‹line››
from assms obtain u v::real where
ne: "x0 ≠ x3" "(1 - u) *⇩R x0 + u *⇩R x3 ≠ x3"
and x1_def: "x1 = (1 - u) *⇩R x0 + u *⇩R x3"
and x2_def: "x2 = (1 - v) *⇩R ((1 - u) *⇩R x0 + u *⇩R x3) + v *⇩R x3"
and uv: ‹0 < u› ‹0 < v› ‹u < 1› ‹v < 1›
by (auto simp: in_segment)
let ?d = "(u + v - u * v)"
have "?d > 0" using uv
with ‹x0 ≠ x3› have "0 ≠ ?d *⇩R (x3 - x0)" by simp
moreover
define ua where "ua = u / ?d"
have "ua * (u * v - u - v) - - u = 0"
by (auto simp: ua_def algebra_simps divide_simps)
mult_less_cancel_left_pos not_real_square_gt_zero vector_space_over_itself.scale_zero_left)
then have "(ua * (u * v - u - v) - - u) *⇩R (x3 - x0) = 0"
by simp
moreover
have "0 < ua" "ua < 1"
using ‹0 < u› ‹0 < v› ‹u < 1› ‹v < 1›
by (auto simp: ua_def pos_add_strict intro!: divide_pos_pos)
ultimately show ?thesis
unfolding x1_def x2_def
by (auto intro!: exI[where x=ua] simp: algebra_simps in_segment)
qed

subsection ‹Syntax›

abbreviation sequentially_at_top::"(nat⇒real)⇒bool"
("_ ⇢⇘⇙ ∞") ― ‹the ‹⇘⇙› is to disambiguate syntax...›
where "s ⇢⇘⇙ ∞  ≡ filterlim s at_top sequentially"

abbreviation sequentially_at_bot::"(nat⇒real)⇒bool"
("_ ⇢⇘⇙ -∞")
where "s ⇢⇘⇙ -∞  ≡ filterlim s at_bot sequentially"

subsection ‹Paths›

lemma subpath0_linepath:
shows "subpath 0 u (linepath t t') = linepath t (t + u * (t' - t))"
unfolding subpath_def linepath_def
apply (rule ext)
apply auto
proof -
fix x :: real
have f1: "⋀r ra rb rc. (r::real) + ra * rb - ra * rc = r - ra * (rc - rb)"
have f2: "⋀r ra. (r::real) - r * ra = r * (1 - ra)"
have f3: "⋀r ra rb. (r::real) - ra + rb + ra - r = rb"
by auto
have f4: "⋀r. (r::real) + (1 - 1) = r"
by linarith
have f5: "⋀r ra. (r::real) + ra = ra + r"
by force
have f6: "⋀r ra. (r::real) + (1 - (r + 1) + ra) = ra"
by linarith
have "t - x * (t - (t + u * (t' - t))) = t' * (u * x) + (t - t * (u * x))"
then show "(1 - u * x) * t + u * x * t' = (1 - x) * t + x * (t + u * (t' - t))"
using f6 f5 f4 f3 f2 f1 by (metis (no_types) mult.commute)
qed

lemma linepath_image0_right_open_real:
assumes "t < (t'::real)"
shows "linepath t t'  {0..<1} = {t..<t'}"
unfolding linepath_def
apply auto
apply (metis add.commute add_diff_cancel_left' assms diff_diff_eq2 diff_le_eq less_eq_real_def mult.commute mult.right_neutral mult_right_mono right_diff_distrib')
apply (smt assms comm_semiring_class.distrib mult_diff_mult semiring_normalization_rules(2) zero_le_mult_iff)
proof -
fix x
assume "t ≤ x" "x < t'"
let ?u = "(x-t)/(t'-t)"
have "?u ≥ 0"
using ‹t ≤ x› assms by auto
moreover have "?u < 1"
by (simp add: ‹x < t'› assms)
moreover have "x = (1-?u) * t + ?u*t'"
proof -
have f1: "∀r ra. (ra::real) * - r = r * - ra"
by simp
have "t + (t' + - t) * ((x + - t) / (t' + - t)) = x"
using assms by force
then have "t' * ((x + - t) / (t' + - t)) + t * (1 + - ((x + - t) / (t' + - t))) = x"
using f1 by (metis (no_types) add.left_commute distrib_left mult.commute mult.right_neutral)
then show ?thesis
qed
ultimately show "x ∈ (λx. (1 - x) * t + x * t')  {0..<1}"
using atLeastLessThan_iff by blast
qed

lemma oriented_subsegment_scale:
assumes "x1 ∈ {a<--<b}"
assumes "x2 ∈ {x1<--<b}"
obtains e where "e > 0" "b-a = e *⇩R (x2-x1)"
proof -
from assms(1) obtain u where u : "u > 0" "u < 1" "x1 = (1 - u) *⇩R a + u *⇩R b"
unfolding in_segment by blast
from assms(2) obtain v where v: "v > 0" "v < 1" "x2 = (1 - v) *⇩R x1 + v *⇩R b"
unfolding in_segment by blast
have "x2-x1 = -v *⇩R x1 + v *⇩R b" using v
also have "... = (-v) *⇩R ((1 - u) *⇩R a + u *⇩R b)  + v *⇩R b" using u by auto
also have "... = v *⇩R ((1-u)*⇩R b - (1-u)*⇩R a )"
finally have x2x1:"x2-x1 = (v *(1-u)) *⇩R (b - a)"
by (metis scaleR_scaleR scale_right_diff_distrib)
have "v * (1-u) > 0"  using u(2) v(1) by simp
then have "(x2-x1)/⇩R (v * (1-u)) = (b-a)" unfolding x2x1
by (smt field_class.field_inverse scaleR_one scaleR_scaleR)
thus ?thesis
using ‹0 < v * (1 - u)› positive_imp_inverse_positive that by fastforce
qed

end


# Theory ODE_Misc

section ‹Additions to the ODE Library›
theory ODE_Misc
imports
Ordinary_Differential_Equations.ODE_Analysis
Analysis_Misc
begin

lemma local_lipschitz_compact_bicomposeE:
assumes ll: "local_lipschitz T X f"
assumes cf: "⋀x. x ∈ X ⟹ continuous_on I (λt. f t x)"
assumes cI: "compact I"
assumes "I ⊆ T"
assumes cv: "continuous_on I v"
assumes cw: "continuous_on I w"
assumes v: "v  I ⊆ X"
assumes w: "w  I ⊆ X"
obtains L where "L > 0" "⋀x. x ∈ I ⟹ dist (f x (v x)) (f x (w x)) ≤ L * dist (v x) (w x)"
proof -
from v w have "v  I ∪ w  I ⊆ X" by auto
with ll ‹I ⊆ T› have llI:"local_lipschitz I (v  I ∪ w  I) f"
by (rule local_lipschitz_subset)
have cvwI: "compact (v  I ∪ w  I)"
by (auto intro!: compact_continuous_image cv cw cI)

from local_lipschitz_compact_implies_lipschitz[OF llI cvwI ‹compact I› cf]
obtain L where L: "⋀t. t ∈ I ⟹ L-lipschitz_on (v  I ∪ w  I) (f t)"
using v w
by blast
define L' where "L' = max L 1"
with L have "L' > 0" "⋀x. x ∈ I ⟹ dist (f x (v x)) (f x (w x)) ≤ L' * dist (v x) (w x)"
apply (auto simp: lipschitz_on_def L'_def)
by (smt Un_iff image_eqI mult_right_mono zero_le_dist)
then show ?thesis ..
qed

subsection ‹Comparison Principle›

lemma comparison_principle_le:
fixes f::"real ⇒ real ⇒ real"
and φ ψ::"real ⇒ real"
assumes ll: "local_lipschitz X Y f"
assumes cf: "⋀x. x ∈ Y ⟹ continuous_on {a..b} (λt. f t x)"
assumes abX: "{a .. b} ⊆ X"
assumes φ': "⋀x. x ∈ {a .. b} ⟹ (φ has_real_derivative φ' x) (at x)"
assumes ψ': "⋀x. x ∈ {a .. b} ⟹ (ψ has_real_derivative ψ' x) (at x)"
assumes φ_in: "φ  {a..b} ⊆ Y"
assumes ψ_in: "ψ  {a..b} ⊆ Y"
assumes init: "φ a ≤ ψ a"
assumes defect: "⋀x. x ∈ {a .. b} ⟹ φ' x - f x (φ x) ≤ ψ' x - f x (ψ x)"
shows "∀x ∈ {a .. b}. φ x ≤ ψ x" (is "?th1")
(*
"(∀x ∈ {a .. b}. φ x < ψ x) ∨ (∃c∈{a..b}. (∀x∈{a..c}. φ x ≤ ψ x) ∧ (∀x∈{c<..b}. φ x < ψ x))"
(is "?th2")
*)
unfolding atomize_conj
apply (cases "a ≤ b")
defer subgoal by simp
proof -
assume "a ≤ b"
note φ_cont = has_real_derivative_imp_continuous_on[OF φ']
note ψ_cont = has_real_derivative_imp_continuous_on[OF ψ']
from local_lipschitz_compact_bicomposeE[OF ll cf compact_Icc abX φ_cont ψ_cont φ_in ψ_in]
obtain L where L: "L > 0" "⋀x. x ∈ {a..b} ⟹ dist (f x (φ x)) (f x (ψ x)) ≤ L * dist (φ x) (ψ x)" by blast
define w where "w x = ψ x - φ x" for x

have w'[derivative_intros]: "⋀x. x ∈ {a .. b} ⟹ (w has_real_derivative ψ' x - φ' x) (at x)"
using φ' ψ'
by (auto simp: has_vderiv_on_def w_def[abs_def] intro!: derivative_eq_intros)
note w_cont[continuous_intros] = has_real_derivative_imp_continuous_on[OF w', THEN continuous_on_compose2]
have "w d ≥ 0" if "d ∈ {a .. b}" for d
proof (rule ccontr, unfold not_le)
assume "w d < 0"
let ?N = "(w - {..0} ∩ {a .. d})"
from ‹w d < 0› that have "d ∈ ?N" by auto
then have "?N ≠ {}" by auto
have "closed ?N"
unfolding compact_eq_bounded_closed
using that
by (intro conjI closed_vimage_Int) (auto intro!: continuous_intros)

let ?N' = "{a0 ∈ {a .. d}. w  {a0 .. d} ⊆ {..0}}"
from ‹w d < 0› that have "d ∈ ?N'" by simp
then have "?N' ≠ {}" by auto
have "compact ?N'"
unfolding compact_eq_bounded_closed
proof
have "?N' ⊆ {a .. d}" using that by auto
then show "bounded ?N'"
by (rule bounded_subset[rotated]) simp
have "w u ≤ 0" if "(∀n. x n ∈ ?N')" "x ⇢ l" "l ≤ u" "u ≤ d" for x l u
proof cases
assume "l = u"
have "∀n. x n ∈ ?N" using that(1) by force
from closed_sequentially[OF ‹closed ?N› this ‹x ⇢ l›]
show ?thesis by (auto simp: ‹l = u›)
next
assume "l ≠ u" with that have "l < u" by auto
from order_tendstoD(2)[OF ‹x ⇢ l› ‹l < u›] obtain n where "x n < u"
by (auto dest: eventually_happens)
with that show ?thesis using ‹l < u›
by (auto dest!: spec[where x=n] simp: image_subset_iff)
qed
then show "closed ?N'"
unfolding closed_sequential_limits
by (auto simp: Lim_bounded Lim_bounded2)
qed

from compact_attains_inf[OF ‹compact ?N'› ‹?N' ≠ {}›]
obtain a0 where a0: "a ≤ a0" "a0 ≤ d" "w  {a0..d} ⊆ {..0}"
and a0_least: "⋀x. a ≤ x ⟹ x ≤ d ⟹ w  {x..d} ⊆ {..0} ⟹ a0 ≤ x"
by auto
have a0d: "{a0 .. d} ⊆ {a .. b}" using that a0
by auto
have L_w_bound: "L * w x ≤ ψ' x - φ' x" if "x ∈ {a0 .. d}" for x
proof -
from set_mp[OF a0d that] have "x ∈ {a .. b}" .
from defect[OF this]
have "φ' x - ψ' x ≤ dist (f x (φ x)) (f x (ψ x))"
also have "… ≤ L * dist (φ x) (ψ x)"
using ‹x ∈ {a .. b}›
by (rule L)
also have "… ≤ -L * w x"
using ‹0 < L› a0 that
by (force simp add: dist_real_def abs_real_def w_def algebra_split_simps )
finally show ?thesis
by simp
qed
have mono: "mono_on (λx. w x * exp(-L*x)) {a0..d}"
apply (rule mono_onI)
apply (rule DERIV_nonneg_imp_nondecreasing, assumption)
using a0d
by (auto intro!: exI[where x="(ψ' x - φ' x) * exp (- (L * x)) - exp (- (L * x)) * L * w x" for x]
derivative_eq_intros L_w_bound simp: )
then have "w a0 * exp (-L * a0) ≤ w d * exp (-L * d)"
by (rule mono_onD) (use that a0 in auto)
also have "… < 0" using ‹w d < 0› by (simp add: algebra_split_simps)
finally have "w a0 * exp (- L * a0) < 0" .
then have "w a0 < 0" by (simp add: algebra_split_simps)
have "a0 ≤ a"
proof (rule ccontr, unfold not_le)
assume "a < a0"
have "continuous_on {a.. a0} w"
by (rule continuous_intros, assumption) (use a0 a0d in auto)
from continuous_on_Icc_at_leftD[OF this ‹a < a0›]
have "(w ⤏ w a0) (at_left a0)" .
from order_tendstoD(2)[OF this ‹w a0 < 0›] have "∀⇩F x in at_left a0. w x < 0" .
moreover have "∀⇩F x in at_left a0. a < x"
by (rule order_tendstoD) (auto intro!: ‹a < a0›)
ultimately have "∀⇩F x in at_left a0. a < x ∧ w x < 0" by eventually_elim auto
then obtain a1' where "a1'<a0" and a1_neg: "⋀y. y > a1' ⟹ y < a0 ⟹ a < y ∧ w y < 0"
unfolding eventually_at_left_field by auto
define a1 where "a1 = (a1' + a0)/2"
have "a1 < a0" using ‹a1' < a0› by (auto simp: a1_def)
have "a ≤ a1"
using ‹a < a0› a1_neg by (force simp: a1_def)
moreover have "a1 ≤ d"
using ‹a1' < a0› a0(2) by (auto simp: a1_def)
moreover have "w  {a1..a0} ⊆ {..0}"
using ‹w a0 < 0› a1_neg a0(3)
by (auto simp: a1_def) smt
moreover have "w  {a0..d} ⊆ {..0}" using a0 by auto
ultimately
have "a0 ≤ a1"
apply (intro a0_least) apply assumption apply assumption
by (smt atLeastAtMost_iff image_subset_iff)
with ‹a1<a0› show False by simp
qed
then have "a0 = a" using ‹a ≤ a0› by simp
with ‹w a0 < 0› have "w a < 0" by simp
with init show False
by (auto simp: w_def)
qed
then show ?thesis
by (auto simp: w_def)
qed

lemma local_lipschitz_mult:
shows "local_lipschitz  (UNIV::real set) (UNIV::real set) (*)"
apply (auto intro!: c1_implies_local_lipschitz[where f'="λp. blinfun_mult_left (fst p)"])
by (auto intro!: continuous_intros)

lemma comparison_principle_le_linear:
fixes φ :: "real ⇒ real"
assumes "continuous_on {a..b} g"
assumes "(⋀t. t ∈ {a..b} ⟹ (φ has_real_derivative φ' t) (at t))"
assumes "φ a ≤ 0"
assumes "(⋀t. t ∈ {a..b} ⟹ φ' t ≤ g t *⇩R φ t)"
shows "∀t∈{a..b}. φ t ≤ 0"
proof -
have *: "⋀x. continuous_on {a..b} (λt. g t * x)"
using assms(1) continuous_on_mult_right by blast
then have "local_lipschitz (g{a..b}) UNIV (*)"
using local_lipschitz_subset[OF local_lipschitz_mult] by blast
from local_lipschitz_compose1[OF this assms(1)]
have "local_lipschitz {a..b} UNIV (λt. (*) (g t))" .
from comparison_principle_le[OF this _ _ assms(2) _ _ _ assms(3), of b "λt.0"] * assms(4)
show ?thesis by auto
qed

subsection ‹Locally Lipschitz ODEs›

context ll_on_open_it begin

lemma flow_lipschitzE:
assumes "{a .. b} ⊆ existence_ivl t0 x"
obtains L where "L-lipschitz_on {a .. b} (flow t0 x)"
proof -
have f': "(flow t0 x has_derivative (λi. i *⇩R f t (flow t0 x t))) (at t within {a .. b})" if "t ∈ {a .. b}" for t
using flow_has_derivative[of t x] assms that
by (auto simp: has_derivative_at_withinI)

have "compact ((λt. f t (flow t0 x t))  {a .. b})"
using assms
apply (auto intro!: compact_continuous_image continuous_intros)
using local.existence_ivl_empty2 apply fastforce
apply (meson atLeastAtMost_iff general.existence_ivl_subset in_mono)
then obtain C where "t ∈ {a .. b} ⟹ norm (f t (flow t0 x t)) ≤ C" for t
by (fastforce dest!: compact_imp_bounded simp: bounded_iff intro: that)
then have "t ∈ {a..b} ⟹ onorm (λi. i *⇩R f t (flow t0 x t)) ≤ max 0 C" for t
apply (subst onorm_scaleR_left)
apply (auto simp: onorm_id max_def)
by (metis diff_0_right diff_mono diff_self norm_ge_zero)
from bounded_derivative_imp_lipschitz[OF f' _ this]
have "(max 0 C)-lipschitz_on {a..b} (flow t0 x)"
by auto
then show ?thesis ..
qed

lemma flow_undefined0: "t ∉ existence_ivl t0 x ⟹ flow t0 x t = 0"
unfolding flow_def by auto

lemma csols_undefined: "x ∉ X ⟹ csols t0 x = {}"
apply (auto simp: csols_def)
using general.existence_ivl_empty2 general.existence_ivl_maximal_segment
apply blast
done

lemmas existence_ivl_undefined = existence_ivl_empty2

end

subsection ‹Reverse flow as Sublocale›

lemma range_preflect_0[simp]: "range (preflect 0) = UNIV"
by (auto simp: preflect_def)
lemma range_uminus[simp]: "range uminus = (UNIV::'a::ab_group_add set)"
by auto

context auto_ll_on_open begin

sublocale rev: auto_ll_on_open "-f" rewrites "-(-f) = f"
apply unfold_locales
using auto_local_lipschitz auto_open_domain
unfolding fun_Compl_def local_lipschitz_minus
by auto

lemma existence_ivl_eq_rev0: "existence_ivl0 y = uminus  rev.existence_ivl0 y" for y
by (auto simp: existence_ivl_eq_rev rev.existence_ivl0_def preflect_def)

lemma rev_existence_ivl_eq0: "rev.existence_ivl0 y = uminus  existence_ivl0 y" for y
using uminus_uminus_image[of "rev.existence_ivl0 y"]

lemma flow_eq_rev0: "flow0 y t = rev.flow0 y (-t)" for y t
apply (cases "t ∈ existence_ivl0 y")
subgoal
apply (subst flow_eq_rev(2), assumption)
apply (subst rev.flow0_def)
subgoal
apply (frule flow_undefined0)
by (auto simp: existence_ivl_eq_rev0 rev.flow_undefined0)
done

lemma rev_eq_flow: "rev.flow0 y t = flow0 y (-t)" for y t
apply (subst flow_eq_rev0)
using uminus_uminus_image[of "rev.existence_ivl0 y"]
apply -
apply (subst (asm) existence_ivl_eq_rev0[symmetric])
by auto

lemma rev_flow_image_eq: "rev.flow0 x  S = flow0 x  (uminus  S)"
unfolding rev_eq_flow[abs_def]
by force

lemma flow_image_eq_rev: "flow0 x  S = rev.flow0 x  (uminus  S)"
unfolding rev_eq_flow[abs_def]
by force

end

context c1_on_open begin

sublocale rev: c1_on_open "-f" "-f'" rewrites "-(-f) = f" and "-(-f') = f'"
by (rule c1_on_open_rev) auto

end

context c1_on_open_euclidean begin

sublocale rev: c1_on_open_euclidean "-f" "-f'" rewrites "-(-f) = f" and "-(-f') = f'"
by unfold_locales auto

end

subsection ‹Autonomous LL ODE : Existence Interval and trapping on the interval›

lemma bdd_above_is_intervalI: "bdd_above I"
if "is_interval I" "a ≤ b" "a ∈ I" "b ∉ I" for I::"real set"
by (meson bdd_above_def is_interval_1 le_cases that)

lemma bdd_below_is_intervalI: "bdd_below I"
if "is_interval I" "a ≤ b" "a ∉ I" "b ∈ I" for I::"real set"
by (meson bdd_below_def is_interval_1 le_cases that)

context auto_ll_on_open begin

lemma open_existence_ivl0:
assumes x : "x ∈ X"
shows "∃a b. a < 0 ∧ 0 < b ∧ {a..b} ⊆ existence_ivl0 x"
proof -
have a1:"0 ∈ existence_ivl0 x"
have a2: "open (existence_ivl0 x)"
from a1 a2 obtain d where "d > 0" "ball 0 d ⊆ existence_ivl0 x"
using openE by blast
have "{-d/2..d/2} ⊆ ball 0 d"
using ‹0 < d› dist_norm mem_ball by auto
thus ?thesis
by (smt ‹0 < d› ‹ball 0 d ⊆ existence_ivl0 x› divide_minus_left half_gt_zero order_trans)
qed

lemma open_existence_ivl':
assumes x : "x ∈ X"
obtains a where "a > 0"  "{-a..a} ⊆ existence_ivl0 x"
proof -
from open_existence_ivl0[OF assms(1)]
obtain a b where ab: "a < 0" "0 < b" "{a..b} ⊆ existence_ivl0 x" by auto
then have "min (-a) b > 0" by linarith
have "{-min (-a) b .. min(-a) b} ⊆ {a..b}" by auto
thus ?thesis using ab(3) that[OF ‹min (-a) b > 0›] by blast
qed

lemma open_existence_ivl_on_compact:
assumes C: "C ⊆ X" and "compact C" "C ≠ {}"
obtains a where "a > 0" "⋀x. x ∈ C ⟹ {-a..a} ⊆ existence_ivl0 x"
proof -
from existence_ivl_cballs
have "∀x∈C. ∃e>0. ∃t>0. ∀y∈cball x e. cball 0 t⊆existence_ivl0 y"
by (metis (full_types) C Int_absorb1 Int_iff UNIV_I)
then
obtain d' t' where *:
"∀x∈C. 0 < d' x ∧ t' x > 0 ∧ (∀y∈cball x (d' x). cball 0 (t' x) ⊆ existence_ivl0 y)"
by metis
with compactE_image[OF ‹compact C›, of C "λx. ball x (d' x)"]
obtain C' where "C' ⊆ C" and [simp]: "finite C'" and C_subset: "C ⊆ (⋃c∈C'. ball c (d' c))"
by force
from C_subset ‹C ≠ {}› have [simp]: "C' ≠ {}" by auto
define d where "d = Min (d'  C')"
define t where "t = Min (t'  C')"
have "t > 0" using * ‹C' ⊆ C›
by (auto simp: t_def)
moreover have "{-t .. t} ⊆ existence_ivl0 x" if "x ∈ C" for x
proof -
from C_subset that ‹C' ⊆ C›
obtain c where c: "c ∈ C'" "x ∈ ball c (d' c)" "c ∈ C" by force
then have "{-t .. t} ⊆ cball 0 (t' c)"
by (auto simp: abs_real_def t_def minus_le_iff)
also
from c have "cball 0 (t' c) ⊆ existence_ivl0 x"
using *[rule_format, OF ‹c ∈ C›] by auto
finally show ?thesis .
qed
ultimately show ?thesis ..
qed

definition "trapped_forward x K ⟷ (flow0 x  (existence_ivl0 x ∩ {0..}) ⊆ K)"
― ‹TODO: use this for backwards trapped, invariant, and all assumptions›

definition "trapped_backward x K ⟷ (flow0 x  (existence_ivl0 x ∩ {..0}) ⊆ K)"

definition "trapped x K ⟷ trapped_forward x K ∧ trapped_backward x K"

lemma trapped_iff_on_existence_ivl0:
"trapped x K ⟷ (flow0 x  (existence_ivl0 x) ⊆ K)"
unfolding trapped_def trapped_forward_def trapped_backward_def
apply (auto)
by (metis IntI atLeast_iff atMost_iff image_subset_iff less_eq_real_def linorder_not_less)
end

context auto_ll_on_open begin

lemma infinite_rev_existence_ivl0_rewrites:
"{0..} ⊆ rev.existence_ivl0 x ⟷ {..0} ⊆ existence_ivl0 x"
"{..0} ⊆ rev.existence_ivl0 x ⟷ {0..} ⊆ existence_ivl0 x"
apply (auto simp add: rev.rev_existence_ivl_eq0 subset_iff)
using neg_le_0_iff_le apply fastforce
using neg_0_le_iff_le by fastforce

lemma trapped_backward_iff_rev_trapped_forward:
"trapped_backward x K  ⟷ rev.trapped_forward x K"
unfolding trapped_backward_def rev.trapped_forward_def
by (auto simp add: rev_flow_image_eq existence_ivl_eq_rev0 image_subset_iff)

text ‹If solution is trapped in a compact set at some time
on its existence interval then it is trapped forever›
lemma trapped_sol_right:
― ‹TODO: when building on afp-devel (??? outdated):
🌐‹https://bitbucket.org/isa-afp/afp-devel/commits/0c3edf9248d5389197f248c723b625c419e4d3eb››
assumes "compact K" "K ⊆ X"
assumes "x ∈ X" "trapped_forward x K"
shows "{0..} ⊆ existence_ivl0 x"
proof (rule ccontr)
assume "¬ {0..} ⊆ existence_ivl0 x"
from this obtain t where "0 ≤ t" "t ∉ existence_ivl0 x" by blast
then have bdd: "bdd_above (existence_ivl0 x)"
by (auto intro!: bdd_above_is_intervalI ‹x ∈ X›)
from flow_leaves_compact_ivl_right [OF UNIV_I ‹x ∈ X› bdd UNIV_I assms(1-2)]
show False by (metis assms(4) trapped_forward_def IntI atLeast_iff image_subset_iff)
qed

lemma trapped_sol_right_gen:
assumes "compact K" "K ⊆ X"
assumes "t ∈ existence_ivl0 x" "trapped_forward (flow0 x t) K"
shows "{t..} ⊆ existence_ivl0 x"
proof -
have "x ∈ X"
using assms(3) local.existence_ivl_empty_iff by fastforce
have xtk: "flow0 x t ∈ X"
from trapped_sol_right[OF assms(1-2) xtk assms(4)] have "{0..} ⊆ existence_ivl0 (flow0 x t)" .
thus "{t..} ⊆ existence_ivl0 x"
using existence_ivl_trans[OF assms(3)]
qed

lemma trapped_sol_left:
― ‹TODO: when building on afp-devel:
🌐‹https://bitbucket.org/isa-afp/afp-devel/commits/0c3edf9248d5389197f248c723b625c419e4d3eb››
assumes "compact K" "K ⊆ X"
assumes "x ∈ X" "trapped_backward x K"
shows "{..0} ⊆ existence_ivl0 x"
proof (rule ccontr)
assume "¬ {..0} ⊆ existence_ivl0 x"
from this obtain t where "t ≤ 0" "t ∉ existence_ivl0 x" by blast
then have bdd: "bdd_below (existence_ivl0 x)"
by (auto intro!: bdd_below_is_intervalI ‹x ∈ X›)
from flow_leaves_compact_ivl_left [OF UNIV_I ‹x ∈ X› bdd UNIV_I assms(1-2)]
show False
by (metis IntI assms(4) atMost_iff auto_ll_on_open.trapped_backward_def auto_ll_on_open_axioms image_subset_iff)
qed

lemma trapped_sol_left_gen:
assumes "compact K" "K ⊆ X"
assumes "t ∈ existence_ivl0 x" "trapped_backward (flow0 x t) K"
shows "{..t} ⊆ existence_ivl0 x"
proof -
have "x ∈ X"
using assms(3) local.existence_ivl_empty_iff by fastforce
have xtk: "flow0 x t ∈ X"
from trapped_sol_left[OF assms(1-2) xtk assms(4)] have "{..0} ⊆ existence_ivl0 (flow0 x t)" .
thus "{..t} ⊆ existence_ivl0 x"
using existence_ivl_trans[OF assms(3)]
qed

lemma trapped_sol:
assumes "compact K" "K ⊆ X"
assumes "x ∈ X" "trapped x K"
shows "existence_ivl0 x = UNIV"
by (metis (mono_tags, lifting) assms existence_ivl_zero image_subset_iff interval local.existence_ivl_initial_time_iff local.existence_ivl_subset local.subset_mem_compact_implies_subset_existence_interval order_refl subset_antisym trapped_iff_on_existence_ivl0)

(* Follows from rectification *)
lemma regular_locally_noteq:― ‹TODO: should be true in ‹ll_on_open_it››
assumes "x ∈ X" "f x ≠ 0"
shows "eventually (λt. flow0 x t ≠ x) (at 0)"
proof -
have nf:"norm (f x) > 0" by (simp add: assms(2))
(* By continuity of solutions and f probably *)
obtain a where
a: "a>0"
"{-a--a} ⊆ existence_ivl0 x"
"0 ∈ {-a--a}"
"⋀t. t ∈ {-a--a} ⟹ norm(f (flow0 x t) - f (flow0 x 0)) ≤ norm(f x)/2"
proof -
from open_existence_ivl'[OF assms(1)]
obtain a1 where a1: "a1 > 0" "{-a1..a1} ⊆ existence_ivl0 x" .
have "continuous (at 0) (λt. norm(f (flow0 x t) - f (flow0 x 0) ))"
apply (auto intro!: continuous_intros)
then obtain a2 where "a2>0"
"∀t. norm t < a2 ⟶
norm (f (flow0 x t) - f (flow0 x 0)) < norm(f x)/2"
unfolding continuous_at_real_range
by (metis abs_norm_cancel cancel_comm_monoid_add_class.diff_cancel diff_zero half_gt_zero nf norm_zero)
then have
t: "⋀t. t ∈ {-a2<--<a2} ⟹ norm(f (flow0 x t) - f (flow0 x 0)) ≤ norm(f x)/2"
by (smt open_segment_bound(2) open_segment_bound1 real_norm_def)
define a where "a = min a1 (a2/2)"
have t1:"a > 0" unfolding a_def using ‹a1 > 0› ‹a2 > 0› by auto
then have t3:"0 ∈{-a--a}"
using closed_segment_eq_real_ivl by auto
have "{-a--a} ⊆ {-a1..a1}" unfolding a_def using ‹a1 > 0› ‹a2 > 0›
using ODE_Auxiliarities.closed_segment_eq_real_ivl by auto
then have t2:"{-a--a} ⊆ existence_ivl0 x" using a1 by auto
have "{-a--a} ⊆ {-a2<--<a2}" unfolding a_def using ‹a1 > 0› ‹a2 > 0›
by (smt Diff_iff closed_segment_eq_real_ivl atLeastAtMost_iff empty_iff half_gt_zero insert_iff pos_half_less segment(1) subset_eq)
then have t4:"⋀t. t ∈ {-a--a} ⟹ norm(f (flow0 x t) - f (flow0 x 0)) ≤ norm(f x)/2" using t by auto
show ?thesis using t1 t2 t3 t4 that by auto
qed
have "⋀t. t ∈ {-a--a} ⟹ (flow0 x has_vector_derivative f (flow0 x t)) (at t within {-a--a})"
apply (rule has_vector_derivative_at_within)
using a(2) by (auto intro!:flow_has_vector_derivative)
from vector_differentiable_bound_linearization[OF this _ a(4)]
have nb:"⋀c d. {c--d} ⊆ {-a--a} ⟹
norm (flow0 x d - flow0 x c - (d - c) *⇩R f (flow0 x 0))  ≤ norm (d - c) * (norm (f x) / 2)"
using a(3) by blast
have "⋀t. dist t 0 < a ⟹ t ≠ 0 ⟹ flow0 x t ≠ x"
proof (rule ccontr)
fix t
assume "dist t 0 < a" "t ≠ 0" "¬ flow0 x t ≠ x"
then have tx:"flow0 x t = x" by auto
have "t ∈ {-a--a}"
using closed_segment_eq_real_ivl ‹dist t 0 < a› by auto
have "t > 0 ∨ t < 0" using ‹t ≠ 0› by linarith
moreover {
assume "t > 0"
then have "{0--t} ⊆ {-a--a}"
by (simp add: ‹t ∈ {-a--a}› a(3) subset_closed_segment)
from nb[OF this] have
"norm (flow0 x t - x - t *⇩R f x) ≤ norm t * (norm (f x) / 2)"
then have "norm (t *⇩R f x) ≤ norm t * (norm (f x) / 2)" using tx by auto
then have False using nf
using ‹0 < t› by auto
}
moreover {
assume "t < 0"
then have "{t--0} ⊆ {-a--a}"
by (simp add: ‹t ∈ {-a--a}› a(3) subset_closed_segment)
from nb[OF this] have
"norm (x - flow0 x t + t *⇩R f x) ≤ norm t * (norm (f x) / 2)"
then have "norm (t *⇩R f x) ≤ norm t * (norm (f x) / 2)" using tx by auto
then have False using nf
using ‹t < 0› by auto
}
ultimately show False by blast
qed
thus ?thesis unfolding eventually_at
using a(1) by blast
qed

lemma compact_max_time_flow_in_closed:
assumes "closed M" and t_ex: "t ∈ existence_ivl0 x"
shows "compact {s ∈ {0..t}. flow0 x  {0..s} ⊆ M}" (is "compact ?C")
unfolding compact_eq_bounded_closed
proof
have "bounded {0 .. t}" by auto
then show "bounded ?C"
by (rule bounded_subset) auto
show "closed ?C"
unfolding closed_def
proof (rule topological_space_class.openI, clarsimp)
― ‹TODO: there must be a more abstract argument for this, e.g., with
@{thm continuous_on_closed_vimageI} and then reasoning about the connected component around 0?›
fix s
assume notM: "s ≤ t ⟶ 0 ≤ s ⟶ ¬ flow0 x  {0..s} ⊆ M"
consider "0 ≤ s" "s ≤ t" "flow0 x s ∉ M" | "0 ≤ s" "s ≤ t" "flow0 x s ∈ M" | "s < 0" | "s > t"
by arith
then show "∃T. open T ∧ s ∈ T ∧ T ⊆ - {s. 0 ≤ s ∧ s ≤ t ∧ flow0 x  {0..s} ⊆ M}"
proof cases
assume s: "0 ≤ s" "s ≤ t" and sM: "flow0 x s ∉ M"
have "isCont (flow0 x) s"
using s ivl_subset_existence_ivl[OF t_ex]
by (auto intro!: flow_continuous)
from this[unfolded continuous_at_open, rule_format, of "-M"] sM ‹closed M›
obtain S where "open S" "s ∈ S" "(∀x'∈S. flow0 x x' ∈ - M)"
by auto
then show ?thesis
by (force intro!: exI[where x=S])
next
assume s: "0 ≤ s" "s ≤ t" and sM: "flow0 x s ∈ M"
from this notM obtain s0 where s0: "0 ≤ s0" "s0 < s" "flow0 x s0 ∉ M"
by force
from order_tendstoD(1)[OF tendsto_ident_at ‹s0 < s›, of UNIV, unfolded eventually_at_topological]
obtain S where "open S" "s ∈ S" "⋀x. x ∈ S ⟹ x ≠ s ⟹ s0 < x"
by auto
then show ?thesis using s0
by (auto simp: intro!: exI[where x=S]) (smt atLeastAtMost_iff image_subset_iff)
qed (force intro: exI[where x="{t<..}"] exI[where x="{..<0}"])+
qed
qed

lemma flow_in_closed_max_timeE:
assumes "closed M" "t ∈ existence_ivl0 x" "0 ≤ t" "x ∈ M"
obtains T where "0 ≤ T" "T ≤ t" "flow0 x  {0..T} ⊆ M"
"⋀s'. 0 ≤ s' ⟹ s' ≤ t ⟹ flow0 x  {0..s'} ⊆ M ⟹ s' ≤ T"
proof -
let ?C = "{s ∈ {0..t}. flow0 x  {0..s} ⊆ M}"
have "?C ≠ {}"
using assms
using local.mem_existence_ivl_iv_defined
by (auto intro!: exI[where x=0])
from compact_max_time_flow_in_closed[OF assms(1,2)]
have "compact ?C" .
from compact_attains_sup[OF this ‹?C ≠ {}›]
obtain s where s: "0 ≤ s" "s ≤ t" "flow0 x  {0..s} ⊆ M"
and s_max: "⋀s'. 0 ≤ s' ⟹ s' ≤ t ⟹ flow0 x  {0..s'} ⊆ M ⟹ s' ≤ s"
by auto
then show ?thesis ..
qed

lemma flow_leaves_closed_at_frontierE:
assumes "closed M" and t_ex: "t ∈ existence_ivl0 x" and "0 ≤ t" "x ∈ M" "flow0 x t ∉ M"
obtains s where "0 ≤ s" "s < t" "flow0 x  {0..s} ⊆ M"
"flow0 x s ∈ frontier M"
"∃⇩F s' in at_right s. flow0 x s' ∉ M"
proof -
from flow_in_closed_max_timeE[OF assms(1-4)] assms(5)
obtain s where s: "0 ≤ s" "s < t" "flow0 x  {0..s} ⊆ M"
and s_max: "⋀s'. 0 ≤ s' ⟹ s' ≤ t ⟹ flow0 x  {0..s'} ⊆ M ⟹ s' ≤ s"
by (smt atLeastAtMost_iff image_subset_iff)
note s
moreover
have "flow0 x s ∉ interior M"
proof
assume interior: "flow0 x s ∈ interior M"
have "s ∈ existence_ivl0 x" using ivl_subset_existence_ivl[OF ‹t ∈ _›] s by auto
from flow_continuous[OF this, THEN isContD, THEN topological_tendstoD, OF open_interior interior]
have "∀⇩F s' in at s. flow0 x s' ∈ interior M" by auto
then have "∀⇩F s' in at_right s. flow0 x s' ∈ interior M"
by (auto simp: eventually_at_split)
moreover have "∀⇩F s' in at_right s. s' < t"
using tendsto_ident_at ‹s < t›
by (rule order_tendstoD)
ultimately have "∀⇩F s' in at_right s. flow0 x s' ∈ M ∧ s' < t"
by eventually_elim (use interior_subset[of M] in auto)
then obtain s' where s': "s < s'" "s' < t" "⋀y. y > s ⟹ y ≤ s' ⟹ flow0 x y ∈ M"
by (auto simp: eventually_at_right_field_le)
have s'_ivl: "flow0 x  {0..s'} ⊆ M"
proof safe
fix s'' assume "s'' ∈ {0 .. s'}"
then show "flow0 x s'' ∈ M"
using s interior_subset[of M] s'
by (cases "s'' ≤ s") auto
qed
with s_max[of s'] ‹s' < t› ‹0 ≤ s› ‹s < s'› show False by auto
qed
then have "flow0 x s ∈ frontier M"
using s closure_subset[of M]
by (force simp: frontier_def)
moreover
have "compact (flow0 x - M ∩ {s..t})" (is "compact ?C")
unfolding compact_eq_bounded_closed
proof
have "bounded {s .. t}" by simp
then show "bounded ?C"
by (rule bounded_subset) auto
show "closed ?C"
using ‹closed M› assms mem_existence_ivl_iv_defined(2)[OF t_ex] ivl_subset_existence_ivl[OF t_ex] ‹0 ≤ s›
by (intro closed_vimage_Int) (auto intro!: continuous_intros)
qed
have "∃⇩F s' in at_right s. flow0 x s' ∉ M"
apply (rule ccontr)
unfolding not_frequently
proof -
assume "∀⇩F s' in at_right s. ¬ flow0 x s' ∉ M"
moreover have "∀⇩F s' in at_right s. s' < t"
using tendsto_ident_at ‹s < t›
by (rule order_tendstoD)
ultimately have "∀⇩F s' in at_right s. flow0 x s' ∈ M ∧ s' < t" by eventually_elim auto
then obtain s' where s': "s < s'"
"⋀y. y > s ⟹ y < s' ⟹ flow0 x y ∈ M"
"⋀y. y > s ⟹ y < s' ⟹ y < t"
by (auto simp: eventually_at_right_field)
define s'' where "s'' = (s + s') / 2"
have "0 ≤ s''" "s'' ≤ t"  "s < s''" "s'' < s'"
using s s'
by (auto simp del: divide_le_eq_numeral1 le_divide_eq_numeral1 simp: s''_def) fastforce
then have "flow0 x  {0..s''} ⊆ M"
using s s'
apply (auto simp: )
subgoal for u
by (cases "u≤s") auto
done
from s_max[OF ‹0 ≤ s''› ‹s''≤ t› this] ‹s'' > s›
show False by simp
qed
ultimately show ?thesis ..
qed

subsection ‹Connectedness›

lemma fcontX:
shows "continuous_on X f"
using auto_local_lipschitz local_lipschitz_continuous_on by blast

lemma fcontx:
assumes "x ∈ X"
shows "continuous (at x) f"
proof -
have "open X" by simp
from continuous_on_eq_continuous_at[OF this]
show ?thesis using fcontX assms(1) by blast
qed

lemma continuous_at_imp_cball:
assumes "continuous (at x) g"
assumes "g x > (0::real)"
obtains r where "r > 0" "∀y ∈ cball x r. g y > 0"
proof -
from assms(1)
obtain d where "d>0" "g  (ball x d) ⊆ ball (g x) ((g x)/2)"
by (meson assms(2) continuous_at_ball half_gt_zero)
then have "∀y ∈ cball x (d/2). g y > 0"
by (smt assms(2) dist_norm image_subset_iff mem_ball mem_cball pos_half_less real_norm_def)
thus ?thesis
using ‹0 < d› that half_gt_zero by blast
qed

text ‹ ‹flow0› is ‹path_connected› ›
lemma flow0_path_connected_time:
assumes "ts ⊆ existence_ivl0 x" "path_connected ts"
shows "path_connected (flow0 x  ts)"
proof -
have "continuous_on ts (flow0 x)"
by (meson assms continuous_on_sequentially flow_continuous_on subsetD)
from path_connected_continuous_image[OF this assms(2)]
show ?thesis .
qed

lemma flow0_path_connected:
assumes "path_connected D"
"path_connected ts"
"⋀x. x ∈ D ⟹ ts ⊆ existence_ivl0 x"
shows "path_connected ( (λ(x, y). flow0 x y)  (D × ts))"
proof -
have "D × ts ⊆ Sigma X existence_ivl0"
using assms(3) subset_iff by fastforce
then have a1:"continuous_on (D × ts) (λ(x, y). flow0 x y)"
using flow_continuous_on_state_space continuous_on_subset by blast
have a2 : "path_connected (D × ts)" using path_connected_Times assms by auto
from path_connected_continuous_image[OF a1 a2]
show ?thesis .
qed

end

subsection ‹Return Time and Implicit Function Theorem›

context c1_on_open_euclidean begin

lemma flow_implicit_function:
― ‹TODO: generalization of @{thm returns_to_implicit_function}!›
fixes s::"'a::euclidean_space ⇒ real" and S::"'a set"
assumes t: "t ∈ existence_ivl0 x" and x: "x ∈ X" and st: "s (flow0 x t) = 0"
assumes Ds: "⋀x. (s has_derivative blinfun_apply (Ds x)) (at x)"
assumes DsC: "isCont Ds (flow0 x t)"
assumes nz: "Ds (flow0 x t) (f (flow0 x t)) ≠ 0"
obtains u e
where "s (flow0 x (u x)) = 0"
"u x = t"
"(⋀y. y ∈ cball x e ⟹ s (flow0 y (u y)) = 0)"
"continuous_on (cball x e) u"
"(λt. (t, u t))  cball x e ⊆ Sigma X existence_ivl0"
"0 < e" "(u has_derivative (- blinfun_scaleR_left
(inverse (blinfun_apply (Ds (flow0 x t)) (f (flow0 x t)))) o⇩L
(Ds (flow0 x t) o⇩L flowderiv x t) o⇩L embed1_blinfun)) (at x)"
proof -
note [derivative_intros] = has_derivative_compose[OF _ Ds]
have cont_s: "continuous_on UNIV s" by (rule has_derivative_continuous_on[OF Ds])
note cls[simp, intro] = closed_levelset[OF cont_s]
then have xt1: "(x, t) ∈ Sigma X existence_ivl0"
by (auto simp: t x)
have D: "(⋀x. x ∈ Sigma X existence_ivl0 ⟹
((λ(x, t). s (flow0 x t)) has_derivative
blinfun_apply (Ds (flow0 (fst x) (snd x)) o⇩L (flowderiv (fst x) (snd x))))
(at x))"
by (auto intro!: derivative_eq_intros)
have C: "isCont (λx. Ds (flow0 (fst x) (snd x)) o⇩L flowderiv (fst x) (snd x))
(x, t)"
using flowderiv_continuous_on[unfolded continuous_on_eq_continuous_within,
rule_format, OF xt1]
using at_within_open[OF xt1 open_state_space]
by (auto intro!: continuous_intros tendsto_eq_intros x t
isCont_tendsto_compose[OF DsC, unfolded poincare_map_def]
simp: split_beta' isCont_def)
have Z: "(case (x, t) of (x, t) ⇒ s (flow0 x t)) = 0"
by (auto simp: st)
have I1: "blinfun_scaleR_left (inverse (Ds (flow0 x t)(f (flow0 x t)))) o⇩L
((Ds (flow0 (fst (x, t))
(snd (x, t))) o⇩L
flowderiv (fst (x, t))
(snd (x, t))) o⇩L
embed2_blinfun)
= 1⇩L"
using nz
by (auto intro!: blinfun_eqI
simp: flowderiv_def blinfun.bilinear_simps inverse_eq_divide poincare_map_def)
have I2: "((Ds (flow0 (fst (x, t))
(snd (x, t))) o⇩L
flowderiv (fst (x, t))
(snd (x, t))) o⇩L
embed2_blinfun) o⇩L blinfun_scaleR_left (inverse (Ds (flow0 x t)(f (flow0 x t))))
= 1⇩L"
using nz
by (auto intro!: blinfun_eqI
simp: flowderiv_def blinfun.bilinear_simps inverse_eq_divide poincare_map_def)
show ?thesis
apply (rule implicit_function_theorem[where f="λ(x, t). s (flow0 x t)"
and S="Sigma X existence_ivl0", OF D xt1 open_state_space order_refl C Z I1 I2])
apply blast
unfolding split_beta' fst_conv snd_conv poincare_map_def[symmetric]
..
qed

lemma flow_implicit_function_at:
fixes s::"'a::euclidean_space ⇒ real" and S::"'a set"
assumes x: "x ∈ X" and st: "s x = 0"
assumes Ds: "⋀x. (s has_derivative blinfun_apply (Ds x)) (at x)"
assumes DsC: "isCont Ds x"
assumes nz: "Ds x (f x) ≠ 0"
assumes pos: "e > 0"
obtains u d
where
"0 < d"
"u x = 0"
"⋀y. y ∈ cball x d ⟹ s (flow0 y (u y)) = 0"
"⋀y. y ∈ cball x d ⟹ ¦u y¦ < e"
"⋀y. y ∈ cball x d ⟹ u y ∈ existence_ivl0 y"
"continuous_on (cball x d) u"
"(u has_derivative -Ds x /⇩R (Ds x) (f x)) (at x)"
proof -
have x0: "flow0 x 0 = x" by (simp add: x)
from flow_implicit_function[OF existence_ivl_zero[OF x] x, unfolded x0, of s, OF st Ds DsC nz]
obtain u d0 where
s0: "s (flow0 x (u x)) = 0"
and u0: "u x = 0"
and u: "⋀y. y ∈ cball x d0 ⟹ s (flow0 y (u y)) = 0"
and uc: "continuous_on (cball x d0) u"
and uex: "(λt. (t, u t))  cball x d0 ⊆ Sigma X existence_ivl0"
and d0: "0 < d0"
and u': "(u has_derivative
blinfun_apply
(- blinfun_scaleR_left (inverse (blinfun_apply (Ds x) (f x))) o⇩L (Ds x o⇩L flowderiv x 0) o⇩L embed1_blinfun))
(at x)"
by blast
have "at x within cball x d0 = at x" by (rule at_within_interior) (auto simp: ‹0 < d0›)
then have "(u ⤏ 0) (at x)"
using uc d0 by (auto simp: continuous_on_def u0 dest!: bspec[where x=x])
from tendstoD[OF this ‹0 < e›] pos u0
obtain d1 where d1: "0 < d1" "⋀xa. dist xa x ≤ d1 ⟹ ¦u xa¦ < e"
unfolding eventually_at_le
by force
define d where "d = min d0 d1"
have "0 < d" by (auto simp: d_def d0 d1)
moreover note u0
moreover have "⋀y. y ∈ cball x d ⟹ s (flow0 y (u y)) = 0" by (auto intro!: u simp: d_def)
moreover have "⋀y. y ∈ cball x d ⟹ ¦u y¦ < e" using d1 by (auto simp: d_def dist_commute)
moreover have "⋀y. y ∈ cball x d ⟹ u y ∈ existence_ivl0 y"
using uex by (force simp: d_def)
moreover have "continuous_on (cball x d) u"
using uc by (rule continuous_on_subset) (auto simp: d_def)
moreover
have "(u has_derivative -Ds x /⇩R (Ds x) (f x)) (at x)"
using u'
by (rule has_derivative_subst) (auto intro!: ext simp: x x0 flowderiv_def blinfun.bilinear_simps)
ultimately show ?thesis ..
qed

lemma returns_to_implicit_function_gen:
― ‹TODO: generalizes proof of @{thm returns_to_implicit_function}!›
fixes s::"'a::euclidean_space ⇒ real"
assumes rt: "returns_to {x ∈ S. s x = 0} x" (is "returns_to ?P x")
assumes cS: "closed S"
assumes Ds: "⋀x. (s has_derivative blinfun_apply (Ds x)) (at x)"
"isCont Ds (poincare_map ?P x)"
"Ds (poincare_map ?P x) (f (poincare_map ?P x)) ≠ 0"
obtains u e
where "s (flow0 x (u x)) = 0"
"u x = return_time ?P x"
"(⋀y. y ∈ cball x e ⟹ s (flow0 y (u y)) = 0)"
"continuous_on (cball x e) u"
"(λt. (t, u t))  cball x e ⊆ Sigma X existence_ivl0"
"0 < e" "(u has_derivative (- blinfun_scaleR_left
(inverse (blinfun_apply (Ds (poincare_map ?P x)) (f (poincare_map ?P x)))) o⇩L
(Ds (poincare_map ?P x) o⇩L flowderiv x (return_time ?P x)) o⇩L embed1_blinfun)) (at x)"
proof -
note [derivative_intros] = has_derivative_compose[OF _ Ds(1)]
have cont_s: "continuous_on UNIV s" by (rule has_derivative_continuous_on[OF Ds(1)])
note cls[simp, intro] = closed_levelset[OF cont_s]
let ?t1 = "return_time ?P x"
have cls[simp, intro]: "closed {x ∈ S. s x = 0}"
by (rule closed_levelset_within) (auto intro!: cS continuous_on_subset[OF cont_s])

have *: "poincare_map ?P x = flow0 x (return_time {x ∈ S. s x = 0} x)"
have "return_time {x ∈ S. s x = 0} x ∈ existence_ivl0 x"
"x ∈ X"
"s (poincare_map ?P x) = 0"
using poincare_map_returns rt
by (auto intro!: return_time_exivl rt)
note E = flow_implicit_function[of "return_time ?P x" x s Ds, OF this[unfolded *] Ds[unfolded *],
folded *]
show ?thesis
by (rule E) rule
qed

text ‹c.f. Perko Section 3.7 Lemma 2 part 1.›

lemma flow_transversal_surface_finite_intersections:
fixes s::"'a ⇒ 'b::real_normed_vector"
and Ds::"'a ⇒ 'a ⇒⇩L 'b"
assumes "closed S"
assumes "⋀x. (s has_derivative (Ds x)) (at x)"
assumes "⋀x. x ∈ S ⟹ s x = 0 ⟹ Ds x (f x) ≠ 0"
assumes "a ≤ b" "{a .. b} ⊆ existence_ivl0 x"
shows "finite {t∈{a..b}. flow0 x t ∈ {x ∈ S. s x = 0}}"
― ‹TODO: define notion of (compact/closed)-(continuous/differentiable/C1)-surface?›
proof cases
note Ds = ‹⋀x. (s has_derivative (Ds x)) (at x)›
note transversal = ‹⋀x. x ∈ S ⟹ s x = 0 ⟹ Ds x (f x) ≠ 0›
assume "a < b"
show ?thesis
proof (rule ccontr)
let ?S = "{x ∈ S. s x = 0}"
let ?T = "{t∈{a..b}. flow0 x t ∈ {x ∈ S. s x = 0}}"
define φ where "φ = flow0 x"
have [THEN continuous_on_compose2, continuous_intros]: "continuous_on S s"
by (auto simp: intro!: has_derivative_continuous_on Ds intro: has_derivative_at_withinI)
assume "infinite ?T"
from compact_sequentialE[OF compact_Icc[of a b] this]
obtain t tl where t: "t n ∈ ?T" "flow0 x (t n) ∈ ?S" "t n ∈ {a .. b}" "t n ≠ tl"
and tl: "t ⇢ tl" "tl ∈ {a..b}"
for n
by force
have tl_ex: "tl ∈ existence_ivl0 x" using ‹{a .. b} ⊆ existence_ivl0 x› ‹tl ∈ {a .. b}› by auto
have "closed ?S"
by (auto intro!: closed_levelset_within ‹closed S› continuous_intros)
moreover
have "∀n. flow0 x (t n) ∈ ?S"
using t by auto
moreover
have flow_t: "(λn. flow0 x (t n)) ⇢ flow0 x tl"
by (auto intro!: tendsto_eq_intros tl_ex tl)
ultimately have "flow0 x tl ∈ ?S"
by (rule closed_sequentially)

let ?qt = "λt. (flow0 x t - flow0 x tl) /⇩R (t - tl)"
from flow_has_vector_derivative[OF tl_ex, THEN has_vector_derivative_withinD]
have qt_tendsto: "?qt ─tl→ f (flow0 x tl)" .
let ?q = "λn. ?qt (t n)"
have "filterlim t (at tl) sequentially"
using tl(1)
by (rule filterlim_atI) (simp add: t)
with qt_tendsto have "?q ⇢ f (flow0 x tl)"
by (rule filterlim_compose)
then have "((λn. Ds (flow0 x tl) (?q n))) ⇢ Ds (flow0 x tl) (f (flow0 x tl))"
by (auto intro!: tendsto_intros)
moreover

from flow_lipschitzE[OF ‹{a .. b} ⊆ existence_ivl0 x›] obtain L' where L': "L'-lipschitz_on {a..b} (flow0 x)" .
define L where "L = L' + 1"
from lipschitz_on_le[OF L', of L] lipschitz_on_nonneg[OF L']
have L: "L-lipschitz_on {a .. b} (flow0 x)" and "L > 0"
by (auto simp: L_def)
from flow_lipschitzE[OF ‹{a .. b} ⊆ existence_ivl0 x›] obtain L' where "L'-lipschitz_on {a..b} (flow0 x)" .
― ‹TODO: is this reasoning (below) with this Lipschitz constant really necessary?›
have s[simp]: "s (flow0 x (t n)) = 0""s (flow0 x tl) = 0"
for n
using t ‹flow0 x tl ∈ ?S›
by auto

from Ds(1)[of "flow0 x tl", unfolded has_derivative_within]
have "(λy. (1 / norm (y - flow0 x tl)) *⇩R (s y - (s (flow0 x tl) + blinfun_apply (Ds (flow0 x tl)) (y - flow0 x tl)))) ─flow0 x tl→ 0"
by auto
then have "((λy. (1 / norm (y - flow0 x tl)) *⇩R (s y - (s (flow0 x tl) + blinfun_apply (Ds (flow0 x tl)) (y - flow0 x tl)))) ⤏ 0)
(nhds (flow0 x tl))"
by (rule tendsto_nhds_continuousI) simp

from filterlim_compose[OF this flow_t]
have "(λxa. (blinfun_apply (Ds (flow0 x tl)) (flow0 x (t xa) - flow0 x tl)) /⇩R norm (flow0 x (t xa) - flow0 x tl))
⇢ 0"
using t
by (auto simp: inverse_eq_divide tendsto_minus_cancel_right)
from tendsto_mult[OF tendsto_const[of "L"] tendsto_norm[OF this, simplified, simplified divide_inverse_commute[symmetric]]]― ‹TODO: uuugly›
have Ds0: "(λxa. norm (blinfun_apply (Ds (flow0 x tl)) (flow0 x (t xa) - flow0 x tl)) / (norm (flow0 x (t xa) - flow0 x tl)/(L))) ⇢ 0"
by (auto simp: ac_simps)

from _ Ds0 have "((λn. Ds (flow0 x tl) (?q n)) ⇢ 0)"
apply (rule Lim_null_comparison)
apply (rule eventuallyI)
unfolding norm_scaleR blinfun.scaleR_right abs_inverse divide_inverse_commute[symmetric]
subgoal for n
apply (cases "flow0 x (t n) = flow0 x tl")
subgoal
apply (rule divide_left_mono)
using lipschitz_onD[OF L, of "t n" tl] ‹0 < L› t(3) tl(2)
by (auto simp: algebra_split_simps zero_less_divide_iff dist_norm pos_divide_le_eq
done
done
ultimately have "Ds (flow0 x tl) (f (flow0 x tl)) = 0"
by (rule LIMSEQ_unique)
moreover have "Ds (flow0 x tl) (f (flow0 x tl)) ≠ 0"
by (rule transversal) (use ‹flow0 x tl ∈ ?S› in auto)
ultimately show False by auto
qed
qed (use assms in auto)

lemma uniform_limit_flow0_state:― ‹TODO: is that something more general?›
assumes "compact C"
assumes "C ⊆ X"
shows "uniform_limit C (λs x. flow0 x s) (λx. flow0 x 0) (at 0)"
proof (cases "C = {}")
case True then show ?thesis by auto
next
case False show ?thesis
proof (rule uniform_limitI)
fix e::real assume "0 < e"
{
fix x assume "x ∈ C"
with assms have "x ∈ X" by auto
from existence_ivl_cballs[OF UNIV_I ‹x ∈ X›]
obtain t L u where "⋀y. y ∈ cball x u ⟹ cball 0 t ⊆ existence_ivl0 y"
"⋀s y. y ∈ cball x u ⟹ s ∈ cball 0 t ⟹ flow0 y s ∈ cball y u"
"L-lipschitz_on (cball 0 t×cball x u) (λ(t, x). flow0 x t)"
"⋀y. y ∈ cball x u ⟹ cball y u ⊆ X"
"0 < t" "0 < u"
by metis
then have "∃L. ∃u>0. ∃t>0. L-lipschitz_on (cball 0 t×cball x u) (λ(t, x). flow0 x t)" by blast
} then have "∀x∈C. ∃L. ∃u>0. ∃t>0. L-lipschitz_on (cball 0 t×cball x u) (λ(t, x). flow0 x t)" ..
then obtain L d' u' where
L: "⋀x. x ∈ C ⟹ (L x)-lipschitz_on (cball 0 (d' x)×cball x (u' x)) (λ(t, x). flow0 x t)"
and d': "⋀x. x ∈ C ⟹ d' x > 0"
and u': "⋀x. x ∈ C ⟹ u' x > 0"
by metis
have "C ⊆ (⋃c∈C. ball c (u' c))" using u' by auto
from compactE_image[OF ‹compact C› _ this]
obtain C' where "C' ⊆ C" and [simp]: "finite C'" and C'_cover: "C ⊆ (⋃c∈C'. ball c (u' c))"
by auto
from C'_cover obtain c' where c': "x ∈ C ⟹ x ∈ ball (c' x) (u' (c' x))" "x ∈ C ⟹ c' x ∈ C'" for x
by (auto simp: subset_iff) metis
have "∀⇩F s in at 0. ∀x∈ball c (u' c). dist (flow0 x s) (flow0 x 0) < e" if "c ∈ C'" for c
proof -
have cC: "c ∈ C"
using c' ‹c ∈ C'› d' ‹C' ⊆ C›
by auto
have *: "dist (flow0 x s) (flow0 x 0) ≤ L c * ¦s¦"
if "x∈ball c (u' c)"
"s ∈ cball 0 (d' c)"
for x s
proof -
from L[OF cC, THEN lipschitz_onD, of "(0, x)" "(s, x)"] d'[OF cC] that
show ?thesis
by (auto simp: dist_prod_def dist_commute)
qed
have "∀⇩F s in at 0. abs s < d' c"
by (rule order_tendstoD tendsto_intros)+ (use d' cC in auto)
moreover have "∀⇩F s in at 0. L c * ¦s¦ < e"
by (rule order_tendstoD tendsto_intros)+ (use ‹0 < e› in auto)
ultimately show ?thesis
apply eventually_elim
apply (use * in auto)
by smt
qed
then have "∀⇩F s in at 0. ∀c∈C'. ∀x∈ball c (u' c). dist (flow0 x s) (flow0 x 0) < e"
then show "∀⇩F s in at 0. ∀x∈C. dist (flow0 x s) (flow0 x 0) < e"
apply eventually_elim
apply (auto simp: )
subgoal for s x
apply (drule bspec[where x="c' x"])
apply (drule bspec) prefer 2 apply assumption
apply auto
using c'(1) by auto
done
qed
qed

end

subsection ‹Fixpoints›

context auto_ll_on_open begin

lemma fixpoint_sol:
assumes "x ∈ X" "f x = 0"
shows "existence_ivl0 x = UNIV" "flow0 x t = x"
proof -
have sol: "((λt::real. x) solves_ode (λ_. f)) UNIV X"
apply (rule solves_odeI)
by(auto simp add: assms intro!: derivative_intros)
from maximal_existence_flow[OF sol] have
"UNIV ⊆ existence_ivl0 x" "flow0 x t = x" by auto
thus "existence_ivl0 x = UNIV" "flow0 x t = x" by auto
qed

end

end

# Theory Invariance

section ‹Invariance›
theory Invariance
imports ODE_Misc
begin

context auto_ll_on_open begin

definition "invariant M ⟷ (∀x∈M. trapped x M)"

definition "positively_invariant M ⟷ (∀x∈M. trapped_forward x M)"

definition "negatively_invariant M ⟷ (∀x∈M. trapped_backward x M)"

lemma positively_invariant_iff:
"positively_invariant M ⟷
(⋃x∈M. flow0 x  (existence_ivl0 x ∩ {0..})) ⊆ M"
unfolding positively_invariant_def trapped_forward_def
by auto

lemma negatively_invariant_iff:
"negatively_invariant M ⟷
(⋃x∈M. flow0 x  (existence_ivl0 x ∩ {..0})) ⊆ M"
unfolding negatively_invariant_def trapped_backward_def
by auto

lemma invariant_iff_pos_and_neg_invariant:
"invariant M ⟷ positively_invariant M ∧ negatively_invariant M"
unfolding invariant_def trapped_def positively_invariant_def negatively_invariant_def
by blast

lemma invariant_iff:
"invariant M ⟷ (⋃x∈M. flow0 x  (existence_ivl0 x)) ⊆  M"
unfolding invariant_iff_pos_and_neg_invariant positively_invariant_iff negatively_invariant_iff
by (metis (mono_tags) SUP_le_iff invariant_def invariant_iff_pos_and_neg_invariant negatively_invariant_iff positively_invariant_iff trapped_iff_on_existence_ivl0)

lemma positively_invariant_restrict_dom: "positively_invariant M = positively_invariant (M ∩ X)"
unfolding positively_invariant_def trapped_forward_def
by (auto intro!: flow_in_domain dest: mem_existence_ivl_iv_defined)

lemma negatively_invariant_restrict_dom: "negatively_invariant M = negatively_invariant (M ∩ X)"
unfolding negatively_invariant_def trapped_backward_def
by (auto intro!: flow_in_domain dest: mem_existence_ivl_iv_defined)

lemma invariant_restrict_dom: "invariant M = invariant (M ∩ X)"
using invariant_iff_pos_and_neg_invariant
negatively_invariant_restrict_dom
positively_invariant_restrict_dom by auto
(*
lemma positively_invariant_imp_subset:
"M ⊆ X" if "positively_invariant M"
using positively_invariant_iff that by blast

lemma negatively_invariant_imp_subset:
"M ⊆ X" if "negatively_invariant M"
using negatively_invariant_iff that by blast

lemma invariant_imp_subset:
"M ⊆ X" if "invariant M"
using invariant_iff that by blast
*)

end context auto_ll_on_open begin

lemma positively_invariant_eq_rev: "positively_invariant M = rev.negatively_invariant M"
unfolding positively_invariant_def rev.negatively_invariant_def

lemma negatively_invariant_eq_rev: "negatively_invariant M = rev.positively_invariant M"
unfolding negatively_invariant_def rev.positively_invariant_def

lemma invariant_eq_rev: "invariant M = rev.invariant M"
unfolding invariant_iff_pos_and_neg_invariant rev.invariant_iff_pos_and_neg_invariant
positively_invariant_eq_rev negatively_invariant_eq_rev by auto

lemma negatively_invariant_complI: "negatively_invariant (X-M)" if "positively_invariant M"
unfolding negatively_invariant_def trapped_backward_def
proof clarsimp
fix x t
assume x: "x ∈ X" "x ∉ M" "t ∈ existence_ivl0 x" "t ≤ 0"
have a1:"flow0 x t ∈ X" using x
using flow_in_domain by blast
have a2:"flow0 x t ∉ M"
proof (rule ccontr)
assume "¬ flow0 x t ∉ M"
then have "trapped_forward (flow0 x t) M"
using positively_invariant_def that by auto
moreover have "flow0 (flow0 x t) (-t) = x"
using ‹t ∈ existence_ivl0 x› flows_reverse by auto
moreover have "-t ∈ existence_ivl0 (flow0 x t) ∩ {0..}"
using existence_ivl_reverse x(3) x(4) by auto
ultimately have "x ∈ M" unfolding trapped_forward_def
by (metis image_subset_iff)
thus False using x(2) by auto
qed
show "flow0 x t ∈ X ∧ flow0 x t ∉ M" using a1 a2 by auto
qed

end context auto_ll_on_open begin

lemma negatively_invariant_complD: "positively_invariant M" if "negatively_invariant (X-M)"
proof -
have "rev.positively_invariant (X-M)" using that
then have "rev.negatively_invariant (X-(X-M))"
then have "positively_invariant (X-(X-M))"
using rev.negatively_invariant_eq_rev by auto
thus ?thesis using Diff_Diff_Int
by (metis inf_commute positively_invariant_restrict_dom)
qed

lemma pos_invariant_iff_compl_neg_invariant: "positively_invariant M ⟷ negatively_invariant (X - M)"
by (safe intro!: negatively_invariant_complI dest!: negatively_invariant_complD)

lemma neg_invariant_iff_compl_pos_invariant:
shows "negatively_invariant M ⟷ positively_invariant (X - M)"
by (simp add: auto_ll_on_open.pos_invariant_iff_compl_neg_invariant negatively_invariant_eq_rev positively_invariant_eq_rev rev.auto_ll_on_open_axioms)

lemma invariant_iff_compl_invariant:
shows "invariant M ⟷ invariant (X - M)"
using invariant_iff_pos_and_neg_invariant neg_invariant_iff_compl_pos_invariant pos_invariant_iff_compl_neg_invariant by blast

lemma invariant_iff_pos_invariant_and_compl_pos_invariant:
shows "invariant M ⟷ positively_invariant M ∧ positively_invariant (X-M)"

end

subsection ‹Tools for proving invariance›

context auto_ll_on_open begin

lemma positively_invariant_left_inter:
assumes "positively_invariant C"
assumes "∀x ∈ C ∩ D. trapped_forward x D"
shows "positively_invariant (C ∩ D)"
using assms positively_invariant_def trapped_forward_def by auto

lemma trapped_forward_le:
fixes V :: "'a ⇒ real"
assumes "V x ≤ 0"
assumes contg: "continuous_on (flow0 x  (existence_ivl0 x ∩ {0..})) g"
assumes "⋀x. (V has_derivative V' x) (at x)"
assumes "⋀s. s ∈ existence_ivl0 x ∩ {0..} ⟹ V' (flow0 x s) (f (flow0 x s)) ≤ g (flow0 x s) * V (flow0 x s)"
shows "trapped_forward x {x. V x ≤ 0}"
unfolding trapped_forward_def
proof clarsimp
fix t
assume t: "t ∈ existence_ivl0 x" "0 ≤ t"
then have ex:"{0..t} ⊆ existence_ivl0 x"
have contV: "continuous_on UNIV V"
using assms(3) has_derivative_continuous_on by blast
have 1: "continuous_on {0..t} (g ∘ flow0 x)"
apply (rule continuous_on_compose)
using continuous_on_subset ex local.flow_continuous_on apply blast
by (meson Int_subset_iff atLeastAtMost_iff atLeast_iff contg continuous_on_subset ex image_mono subsetI)
have 2: "(⋀s. s ∈ {0..t} ⟹
(V ∘ flow0 x has_real_derivative (V' (flow0 x s) ∘ f ∘ flow0 x) s) (at s))"
proof -
fix s
assume "0 ≤ s" "s ≤ t"
then have "s ∈ existence_ivl0 x" using ex by auto
from flow_has_derivative[OF this] have
"(flow0 x has_derivative (λi. i *⇩R f (flow0 x s))) (at s)" .
from has_derivative_compose[OF this assms(3)]
have "((λt. V (flow0 x t)) has_derivative (λt. V' (flow0 x s)  (t *⇩R f (flow0 x s)))) (at s)" .
moreover have "linear (V' (flow0 x s))"  using assms(3) has_derivative_linear by blast
ultimately
have "((λt. V (flow0 x t)) has_derivative (λt. t *⇩R V' (flow0 x s) (f (flow0 x s)))) (at s)"
unfolding linear_cmul[OF ‹linear (V' (flow0 x s))›] by blast
thus "((λt. V (flow0 x t)) has_derivative (*) (V' (flow0 x s) (f (flow0 x s)))) (at s)"
by (auto intro!: derivative_eq_intros simp add: mult_commute_abs)
qed
have 3: "(⋀s. s ∈ {0..t} ⟹
(V' (flow0 x s)  ∘ f ∘ flow0 x) s ≤ (g ∘ flow0 x) s *⇩R (V ∘ flow0 x) s)"
using ex by (auto intro!:assms(4))
from comparison_principle_le_linear[OF 1 2 _ 3] assms(1)
have "∀s ∈ {0..t}. (V ∘ flow0 x) s ≤ 0"
using local.mem_existence_ivl_iv_defined(2) t(1) by auto
thus " V (flow0 x t) ≤ 0"
qed

lemma positively_invariant_le_domain:
fixes V :: "'a ⇒ real"
assumes "positively_invariant D"
assumes contg: "continuous_on D g"
assumes "⋀x. (V has_derivative V' x) (at x)" (* TODO: domain can be added here too ? *)
assumes "⋀s. s ∈ D ⟹ V' s (f s) ≤ g s * V s"
shows "positively_invariant (D ∩ {x. V x ≤ 0})"
apply (auto intro!:positively_invariant_left_inter[OF assms(1)])
proof -
fix x
assume "x ∈ D" "V x ≤ 0"
have "continuous_on (flow0 x  (existence_ivl0 x ∩ {0..})) g"
by (meson ‹x ∈ D› assms(1) contg continuous_on_subset positively_invariant_def trapped_forward_def)
from trapped_forward_le[OF ‹V x ≤ 0› this assms(3)]
show "trapped_forward x {x. V x ≤ 0}" using assms(4)
using ‹x ∈ D› assms(1) positively_invariant_def trapped_forward_def by auto
qed

lemma positively_invariant_barrier_domain:
fixes V :: "'a ⇒ real"
assumes "positively_invariant D"
assumes "⋀x. (V has_derivative V' x) (at x)"
assumes "continuous_on D (λx. V' x (f x))"
assumes "⋀s. s ∈ D ⟹ V s = 0 ⟹ V' s (f s) < 0"
shows "positively_invariant (D ∩ {x. V x ≤ 0})"
apply (auto intro!:positively_invariant_left_inter[OF assms(1)])
proof -
fix x
assume "x ∈ D" "V x ≤ 0"
have contV: "continuous_on UNIV V" using assms(2) has_derivative_continuous_on by blast
then have *: "continuous_on (flow0 x  (existence_ivl0 x ∩ {0..})) V"
using continuous_on_subset by blast
have sub: "flow0 x  (existence_ivl0 x ∩ {0..}) ⊆ D"
using ‹x ∈ D› assms(1) positively_invariant_def trapped_forward_def by auto
then have contV': "continuous_on (flow0 x  (existence_ivl0 x ∩ {0..})) (λx. V' x (f x))"
by (metis assms(3) continuous_on_subset)
have nz: "⋀i t. t ∈ existence_ivl0 x ⟹
0 ≤ t ⟹  max (-V' (flow0 x t) (f (flow0 x t))) ((V (flow0 x t))⇧2) > 0"
proof -
fix i t
assume "t ∈ existence_ivl0 x" "0 ≤ t"
then have "flow0 x t ∈ D"
using ‹x ∈ D› assms(1) positively_invariant_def trapped_forward_def by auto
then have "V (flow0 x t) = 0 ⟹ - V' (flow0 x t) (f (flow0 x t)) > 0" using assms(4) by simp
then have "(V (flow0 x t))^2 > 0 ∨ - V' (flow0 x t) (f (flow0 x t)) > 0" by simp
thus "max (-V' (flow0 x t) (f (flow0 x t))) ((V (flow0 x t))⇧2) > 0" unfolding less_max_iff_disj
by auto
qed
have *: "continuous_on (flow0 x  (existence_ivl0 x ∩ {0..})) (λx. V' x (f x) * V x / max (- V' x (f x)) ((V x)^2))"
apply (auto intro!:continuous_intros continuous_on_max simp add: * contV')
using nz by fastforce
have "(⋀t. t ∈ existence_ivl0 x ∩ {0..} ⟹
V' (flow0 x t) (f (flow0 x t)) ≤
(V' (flow0 x t) (f (flow0 x t)) * V (flow0 x t)
/ max (- V' (flow0 x t) (f (flow0 x t))) ((V (flow0 x t))⇧2)) * V (flow0 x t))"
proof clarsimp
fix t
assume "t ∈ existence_ivl0 x" "0 ≤ t"
then have p: "max (-V' (flow0 x t) (f (flow0 x t))) ((V (flow0 x t))⇧2) > 0" using nz by auto
have " V' (flow0 x t) (f (flow0 x t)) * max (- V' (flow0 x t) (f (flow0 x t))) ((V (flow0 x t))⇧2)
≤  V' (flow0 x t) (f (flow0 x t)) * (V (flow0 x t))⇧2"
by (smt mult_minus_left mult_minus_right power2_eq_square mult_le_cancel_iff2)
then have "V' (flow0 x t) (f (flow0 x t))
≤  V' (flow0 x t) (f (flow0 x t)) * (V (flow0 x t))⇧2
/ max (- V' (flow0 x t) (f (flow0 x t))) ((V (flow0 x t))⇧2)"
using p pos_le_divide_eq by blast
thus " V' (flow0 x t) (f (flow0 x t))
≤ V' (flow0 x t) (f (flow0 x t)) * (V (flow0 x t)) * V (flow0 x t) /
max (- V' (flow0 x t) (f (flow0 x t))) ((V (flow0 x t))⇧2)"
qed
from trapped_forward_le[OF ‹V x ≤ 0› * assms(2) this]
show "trapped_forward x {x. V x ≤ 0}" by auto
qed

lemma positively_invariant_UNIV:
shows "positively_invariant UNIV"
using positively_invariant_iff by blast

lemma positively_invariant_conj:
assumes "positively_invariant C"
assumes "positively_invariant D"
shows "positively_invariant (C ∩ D)"
using assms positively_invariant_def
using positively_invariant_left_inter by auto

lemma positively_invariant_le:
fixes V :: "'a ⇒ real"
assumes contg: "continuous_on UNIV g"
assumes "⋀x. (V has_derivative V' x) (at x)"
assumes "⋀s. V' s (f s) ≤ g s * V s"
shows "positively_invariant {x. V x ≤ 0}"
proof -
from positively_invariant_le_domain[OF positively_invariant_UNIV assms]
have "positively_invariant (UNIV ∩ {x. V x ≤ 0})" .
thus ?thesis by auto
qed

lemma positively_invariant_barrier:
fixes V :: "'a ⇒ real"
assumes "⋀x. (V has_derivative V' x) (at x)"
assumes "continuous_on UNIV (λx. V' x (f x))"
assumes "⋀s. V s = 0 ⟹ V' s (f s) < 0"
shows "positively_invariant {x. V x ≤ 0}"
proof -
from positively_invariant_barrier_domain[OF positively_invariant_UNIV assms]
have "positively_invariant (UNIV ∩ {x. V x ≤ 0})" .
thus ?thesis by auto
qed

end

end

# Theory Limit_Set

section ‹Limit Sets›
theory Limit_Set
imports Invariance
begin

context auto_ll_on_open begin
text ‹Positive limit point, assuming ‹{0..} ⊆ existence_ivl0 x››

(* TODO: Perhaps a more intrinsic definition would be better here *)
definition "ω_limit_point x p ⟷
{0..} ⊆ existence_ivl0 x ∧
(∃s. s ⇢⇘⇙ ∞ ∧ (flow0 x ∘ s) ⇢ p)"

text ‹ Also called the ‹ω›-limit set of x ›
definition "ω_limit_set x = {p. ω_limit_point x p}"

definition "α_limit_point x p ⟷
{..0} ⊆ existence_ivl0 x ∧
(∃s. s ⇢⇘⇙ -∞ ∧ (flow0 x ∘ s) ⇢ p)"

text ‹ Also called the ‹α›-limit set of x ›
definition "α_limit_set x =
{p. α_limit_point x p}"

end context auto_ll_on_open begin

lemma α_limit_point_eq_rev: "α_limit_point x p = rev.ω_limit_point x p"
unfolding α_limit_point_def rev.ω_limit_point_def
apply (auto simp: rev_eq_flow[abs_def] o_def filterlim_uminus_at_bot rev_existence_ivl_eq0 subset_iff
intro: exI[where x="uminus o s" for s])
using neg_0_le_iff_le by fastforce

lemma α_limit_set_eq_rev: "α_limit_set x = rev.ω_limit_set x"
unfolding α_limit_set_def rev.ω_limit_set_def α_limit_point_eq_rev ..

lemma ω_limit_pointE:
assumes "ω_limit_point x p"
obtains s where
"filterlim s at_top sequentially"
"(flow0 x ∘ s) ⇢ p"
"∀n. b ≤ s n"
using assms filterlim_at_top_choose_lower ω_limit_point_def by blast

lemma ω_limit_set_eq:
assumes "{0..} ⊆ existence_ivl0 x"
shows "ω_limit_set x = (INF τ ∈ {0..}. closure (flow0 x  {τ..}))"
unfolding ω_limit_set_def
proof safe
fix p t
assume pt: "0 ≤ (t::real)" "ω_limit_point x p"
from ω_limit_pointE[OF pt(2)]
obtain s where
"filterlim s at_top sequentially"
"(flow0 x ∘ s) ⇢ p"
"∀n. t ≤ s n" by blast
thus "p ∈ closure (flow0 x  {t..})" unfolding closure_sequential
by (metis atLeast_iff comp_apply imageI)
next
fix p
assume "p ∈ (⋂τ∈{0..}. closure (flow0 x  {τ..}))"
then have "⋀t. t ≥0 ⟹ p ∈ closure (flow0 x  {t..})" by blast
then have "⋀t e. t ≥0 ⟹ e > 0 ⟹ (∃tt ≥ t. dist (flow0 x tt) p < e)"
unfolding closure_approachable
by fastforce
from approachable_sequenceE[OF this]
obtain s where "filterlim s at_top sequentially" "(flow0 x ∘ s) ⇢ p" by auto
thus "ω_limit_point x p" unfolding ω_limit_point_def using assms by auto
qed

lemma ω_limit_set_empty:
assumes "¬ ({0..} ⊆ existence_ivl0 x)"
shows "ω_limit_set x = {}"
unfolding ω_limit_set_def ω_limit_point_def

lemma ω_limit_set_closed: "closed (ω_limit_set x)"
using ω_limit_set_eq
by (metis ω_limit_set_empty closed_INT closed_closure closed_empty)

(* TODO: Walter gives a more direct proof *)
lemma ω_limit_set_positively_invariant:
shows "positively_invariant (ω_limit_set x)"
unfolding positively_invariant_def trapped_forward_def
proof safe
fix dummy p t
assume xa: "p ∈ ω_limit_set x"
"t ∈ existence_ivl0 p"
"0 ≤ t"
have "p ∈ X" using mem_existence_ivl_iv_defined(2) xa(2) by blast
have exist: "{0..} ⊆ existence_ivl0 x" using xa(1)
unfolding ω_limit_set_def ω_limit_point_def by auto
from xa(1)
obtain s where s:
"filterlim s at_top sequentially"
"(flow0 x ∘ s) ⇢ p"
"∀n. 0 ≤ s n"
unfolding ω_limit_set_def by (auto elim!:ω_limit_pointE)
define r where "r = (λn. t + s n)"
have rlim: "filterlim r at_top sequentially" unfolding r_def
by (auto intro: filterlim_tendsto_add_at_top[OF _ s(1)])
define dom where "dom = image (flow0 x) {0..} ∪ {p} "
have domin: "∀n. (flow0 x ∘ s) n ∈ dom" "p ∈ dom" unfolding dom_def o_def
using exist by(auto simp add: s(3))
have xt: "⋀x. x ∈ dom ⟹ t ∈ existence_ivl0 x" unfolding dom_def using xa(2)
apply auto
apply (rule existence_ivl_trans')
using exist xa(3) apply auto
using exist  by auto
have cont: "continuous_on dom (λx. flow0 x t)"
apply (rule flow_continuous_on_compose)
apply auto
using ‹p ∈ X›  exist local.dom_def local.flow_in_domain apply auto
using xt .
then have f1: "((λx. flow0 x t) ∘ (flow0 x ∘ s)) ⇢ flow0 p t" using domin s(2)
unfolding continuous_on_sequentially
by blast
have ff:"⋀n. (flow0 x ∘ r) n = ((λx. flow0 x t) ∘ (flow0 x ∘ s)) n"
unfolding o_def r_def
proof -
fix n
have s:"s n ∈ existence_ivl0 x"
using s(3) exist by auto
then have t:"t ∈ existence_ivl0 (flow0 x (s n))"
using domin(1) xt by auto
from flow_trans[OF s t]
show "flow0 x (t + s n) = flow0 (flow0 x (s n)) t"
qed
have f2: "(flow0 x ∘ r) ⇢ flow0 p t" using f1 unfolding ff .
show "flow0 p t ∈ ω_limit_set x" using exist f2 rlim
unfolding ω_limit_set_def ω_limit_point_def
using flow_in_domain r_def s(3) xa(2) xa(3) by auto
qed

lemma ω_limit_set_invariant:
shows "invariant (ω_limit_set x)"
unfolding invariant_iff_pos_invariant_and_compl_pos_invariant
proof safe
show "positively_invariant (ω_limit_set x)"
using ω_limit_set_positively_invariant .
next
show "positively_invariant (X - ω_limit_set x)"
unfolding positively_invariant_def trapped_forward_def
apply safe
using local.flow_in_domain apply blast
proof -
fix dummy p t
assume xa: "p ∈ X" "p ∉ ω_limit_set x"
"t ∈ existence_ivl0 p" "0 ≤ t"
and f: "flow0 p t ∈ ω_limit_set x"
have exist: "{0..} ⊆ existence_ivl0 x" using f
unfolding ω_limit_set_def ω_limit_point_def by auto
from f
obtain s where s:
"filterlim s at_top sequentially"
"(flow0 x ∘ s) ⇢ flow0 p t"
"∀n. t ≤ s n"
unfolding ω_limit_set_def by (auto elim!:ω_limit_pointE)
define r where "r = (λn. (-t) + s n)"
have "(λx. -t) ⇢ -t" by simp
have rlim: "filterlim r at_top sequentially" unfolding r_def by simp
define dom where "dom = image (flow0 x) {t..} ∪ {flow0 p t} "
have domin: "∀n. (flow0 x ∘ s) n ∈ dom" "flow0 p t ∈ dom" unfolding dom_def o_def
using exist by(auto simp add: s(3))
have xt: "⋀x. x ∈ dom ⟹ -t ∈ existence_ivl0 x" unfolding dom_def using xa(2)
apply auto
using local.existence_ivl_reverse xa(3) apply auto
have cont: "continuous_on dom (λx. flow0 x (-t))"
apply (rule flow_continuous_on_compose)
apply auto
using local.mem_existence_ivl_iv_defined(2) xt apply blast
then have f1: "((λx. flow0 x (-t)) ∘ (flow0 x ∘ s)) ⇢ flow0 (flow0 p t) (-t)" using domin s(2)
unfolding continuous_on_sequentially
by blast
have ff:"⋀n. (flow0 x ∘ r) n = ((λx. flow0 x (-t)) ∘ (flow0 x ∘ s)) n"
unfolding o_def r_def
proof -
fix n
have s:"s n ∈ existence_ivl0 x"
using s(3) exist ‹0≤ t› by (meson atLeast_iff order_trans subset_eq)
then have t:"-t ∈ existence_ivl0 (flow0 x (s n))"
using domin(1) xt by auto
from flow_trans[OF s t]
show "flow0 x (-t + s n) = flow0 (flow0 x (s n)) (-t)"
qed
have "(flow0 x ∘ r) ⇢ flow0 (flow0 p t) (-t)" using f1 unfolding ff .
then have f2: "(flow0 x ∘ r) ⇢ p" using flows_reverse xa(3) by auto
then have "p ∈ ω_limit_set x" unfolding ω_limit_set_def ω_limit_point_def
using rlim exist by auto
thus False using xa(2) by auto
qed
qed

end context auto_ll_on_open begin

lemma α_limit_set_eq:
assumes "{..0} ⊆ existence_ivl0 x"
shows "α_limit_set x = (INF τ ∈ {..0}. closure (flow0 x  {..τ}))"
using rev.ω_limit_set_eq[of x, OF assms[folded infinite_rev_existence_ivl0_rewrites]]
unfolding α_limit_set_eq_rev rev_flow_image_eq image_uminus_atLeast
by (smt INT_extend_simps(10) Sup.SUP_cong image_uminus_atMost)

lemma α_limit_set_closed:
shows "closed (α_limit_set x)"
unfolding α_limit_set_eq_rev by (rule rev.ω_limit_set_closed)

lemma α_limit_set_positively_invariant:
shows "negatively_invariant (α_limit_set x)"
unfolding negatively_invariant_eq_rev α_limit_set_eq_rev

lemma α_limit_set_invariant:
shows "invariant (α_limit_set x)"
unfolding invariant_eq_rev α_limit_set_eq_rev

text ‹ Fundamental properties of the positive limit set ›

context
fixes x K
assumes K: "compact K" "K ⊆ X"
assumes x: "x ∈ X" "trapped_forward x K"
begin

text ‹Bunch of facts for what's to come›
private lemma props:
shows "{0..} ⊆ existence_ivl0 x" "seq_compact K"
apply (rule trapped_sol_right)
using x K by (auto simp add: compact_imp_seq_compact)

private lemma flowimg:
shows "flow0 x  (existence_ivl0 x ∩ {0..}) = flow0 x  {0..}"
using props(1) by auto

lemma ω_limit_set_in_compact_subset:
shows "ω_limit_set x ⊆ K"
unfolding ω_limit_set_def
proof safe
fix p s
assume "ω_limit_point x p"
from ω_limit_pointE[OF this]
obtain s where s:
"filterlim s at_top sequentially"
"(flow0 x ∘ s) ⇢ p"
"∀n. 0 ≤ s n" by blast
then have fin: "∀n. (flow0 x ∘ s) n ∈ K" using s(3) x K props(1)
unfolding trapped_forward_def
from seq_compactE[OF props(2) fin]
show "p ∈ K" using s(2)
by (metis LIMSEQ_subseq_LIMSEQ LIMSEQ_unique)
qed

lemma ω_limit_set_in_compact_compact:
shows "compact (ω_limit_set x)"
proof -
from ω_limit_set_in_compact_subset
have "bounded (ω_limit_set x)"
using bounded_subset compact_imp_bounded
using K(1) by auto
thus ?thesis using ω_limit_set_closed
qed

lemma ω_limit_set_in_compact_nonempty:
shows "ω_limit_set x ≠ {}"
proof -
have fin: "∀n. (flow0 x ∘ real) n ∈ K" using x K props(1)
by (simp add: flowimg image_subset_iff trapped_forward_def)
from seq_compactE[OF props(2) this]
obtain r l where "l ∈ K" "strict_mono r" "(flow0 x ∘ real ∘ r) ⇢ l" by blast
then have "ω_limit_point x l" unfolding ω_limit_point_def using props(1)
by (smt comp_def filterlim_sequentially_iff_filterlim_real filterlim_subseq tendsto_at_top_eq_left)
thus ?thesis unfolding ω_limit_set_def by auto
qed

lemma ω_limit_set_in_compact_existence:
shows "⋀y. y ∈ ω_limit_set x ⟹ existence_ivl0 y = UNIV"
proof -
fix y
assume y: "y ∈ ω_limit_set x"
then have "y ∈ X" using ω_limit_set_in_compact_subset K by blast
from ω_limit_set_invariant
have "⋀t. t ∈ existence_ivl0 y ⟹ flow0 y t ∈ ω_limit_set x"
unfolding invariant_def trapped_iff_on_existence_ivl0 using y by blast
then have t: "⋀t. t ∈ existence_ivl0 y ⟹ flow0 y t ∈ K"
using ω_limit_set_in_compact_subset by blast
thus "existence_ivl0 y = UNIV"
by (meson ‹y ∈ X› existence_ivl_zero existence_ivl_initial_time_iff existence_ivl_subset mem_compact_implies_subset_existence_interval subset_antisym K)
qed

lemma ω_limit_set_in_compact_tendsto:
shows "((λt. infdist (flow0 x t) (ω_limit_set x)) ⤏ 0) at_top"
proof (rule ccontr)
assume "¬ ((λt. infdist (flow0 x t) (ω_limit_set x)) ⤏ 0) at_top"
from not_tendsto_frequentlyE[OF this]
obtain S where S: "open S" "0 ∈ S"
"∃⇩F t in at_top. infdist (flow0 x t) (ω_limit_set x) ∉ S" .
then obtain e where "e > 0" "ball 0 e ⊆ S" using openE by blast
then have "⋀x. x ≥0 ⟹ x ∉ S ⟹ x ≥ e" by force
then have "∀xa. infdist (flow0 x xa) (ω_limit_set x) ∉ S ⟶
infdist (flow0 x xa) (ω_limit_set x) ≥ e" using infdist_nonneg by blast
from frequently_mono[OF this S(3)]
have "∃⇩F t in at_top. infdist (flow0 x t) (ω_limit_set x) ≥ e" by blast
then have "∀n. ∃⇩F t in at_top. infdist (flow0 x t) (ω_limit_set x) ≥ e ∧ real n ≤ t"
by (auto intro!: eventually_frequently_conj)
from frequently_at_topE[OF this]
obtain s where s: "⋀i. e ≤ infdist (flow0 x (s i)) (ω_limit_set x)"
"⋀i. real i ≤ s i" "strict_mono s" by force
then have sf: "filterlim s at_top sequentially"
using filterlim_at_top_mono filterlim_real_sequentially not_eventuallyD by blast
have fin: "∀n. (flow0 x ∘ s) n ∈ K"  using x K props(1) s unfolding flowimg trapped_forward_def
by (metis atLeast_iff comp_apply image_subset_iff of_nat_0_le_iff order_trans)
from seq_compactE[OF props(2) this]
obtain r l where r:"strict_mono r" and l: "l ∈ K" "(flow0 x ∘ s ∘ r) ⇢ l" by blast
moreover from filterlim_at_top_strict_mono[OF s(3) r(1) sf]
have "filterlim (s ∘ r) at_top sequentially" .
moreover have "ω_limit_point x l" unfolding ω_limit_point_def using props(1) calculation
by (metis comp_assoc)
ultimately have "infdist l (ω_limit_set x) = 0" by (simp add: ω_limit_set_def)
then have c1:"((λy. infdist y (ω_limit_set x)) ∘ (flow0 x ∘ s ∘ r)) ⇢ 0"
by (auto intro!: tendsto_compose_at[OF l(2)] tendsto_eq_intros)
have c2: "⋀i. e ≤ infdist (flow0 x ((s ∘ r) i)) (ω_limit_set x)" using s(1) by simp
show False using c1 c2 ‹e > 0› unfolding o_def
using Lim_bounded2
by (metis (no_types, lifting) ball_eq_empty centre_in_ball empty_iff)
qed

lemma ω_limit_set_in_compact_connected:
shows "connected (ω_limit_set x)"
unfolding connected_closed_set[OF ω_limit_set_closed]
proof clarsimp
fix Apre Bpre
assume pre: "closed Apre" "Apre ∪ Bpre = ω_limit_set x" "closed Bpre"
"Apre ≠ {}" "Bpre ≠ {}" "Apre ∩ Bpre = {}"
(* TODO: this move is very strange *)
then obtain A B where "Apre ⊆ A" "Bpre ⊆ B" "open A" "open B" and disj:"A ∩ B = {}"
by (meson t4_space)
then have "ω_limit_set x ⊆ A ∪ B"
"ω_limit_set x ∩ A ≠ {}" "ω_limit_set x ∩ B ≠ {}" using pre by auto
then obtain p q where
p: "ω_limit_point x p" "p ∈ A"
and q: "ω_limit_point x q" "q ∈ B"
using ω_limit_set_def by auto
from ω_limit_pointE[OF p(1)]
obtain ps where ps: "filterlim ps at_top sequentially"
"(flow0 x ∘ ps) ⇢ p" "∀n. 0 ≤ ps n" by blast
from ω_limit_pointE[OF q(1)]
obtain qs where qs: "filterlim qs at_top sequentially"
"(flow0 x ∘ qs) ⇢ q" "∀n. 0 ≤ qs n" by blast
have "∀n. ∃⇩F t in at_top. flow0 x t ∉ A ∧ flow0 x t ∉ B" unfolding frequently_at_top
proof safe
fix dummy mpre
obtain m where "m ≥ (0::real)" "m > mpre"
by (meson approximation_preproc_push_neg(1) gt_ex le_cases order_trans)
from ps obtain a where a:"a > m" "(flow0 x a) ∈ A"
using ‹open A› p unfolding tendsto_def filterlim_at_top eventually_sequentially
by (metis approximation_preproc_push_neg(1) comp_apply gt_ex le_cases order_trans)
from qs obtain b where b:"b > a" "(flow0 x b) ∈ B"
using ‹open B› q unfolding tendsto_def filterlim_at_top eventually_sequentially
by (metis approximation_preproc_push_neg(1) comp_apply gt_ex le_cases order_trans)
have "continuous_on {a..b} (flow0 x)"
by (metis Icc_subset_Ici_iff ‹0 ≤ m› ‹m < a› approximation_preproc_push_neg(2) atMost_iff atMost_subset_iff continuous_on_subset le_cases local.flow_continuous_on props(1) subset_eq)
from connected_continuous_image[OF this connected_Icc]
have c:"connected (flow0 x  {a..b})" .
have "∃t∈ {a..b}. flow0 x t ∉ A ∧ flow0 x t ∉ B"
proof (rule ccontr)
assume "¬ (∃t∈{a..b}. flow0 x t ∉ A ∧ flow0 x t ∉ B)"
then have "flow0 x  {a..b} ⊆ A ∪ B" by blast
from topological_space_class.connectedD[OF c ‹open A› ‹open B› _ this]
show False using a b disj by force
qed
thus "∃n>mpre. flow0 x n ∉ A ∧ flow0 x n ∉ B"
by (smt ‹mpre < m› a(1) atLeastAtMost_iff)
qed
from frequently_at_topE'[OF this filterlim_real_sequentially]
obtain s where s: "∀i. flow0 x (s i) ∉ A ∧ flow0 x (s i) ∉ B"
"strict_mono s" "⋀n. real n ≤ s n" by blast
then have "∀n. (flow0 x ∘ s) n ∈ K"
by (smt atLeast_iff comp_apply flowimg image_subset_iff of_nat_0_le_iff trapped_forward_def x(2))
from seq_compactE[OF props(2) this]
obtain r l where r: "l ∈ K" "strict_mono r" "(flow0 x ∘ s ∘ r) ⇢ l" by blast
have "filterlim s at_top sequentially"
using s filterlim_at_top_mono filterlim_real_sequentially not_eventuallyD by blast
from filterlim_at_top_strict_mono[OF s(2) r(2) this]
have "filterlim (s ∘ r) at_top sequentially" .
then have "ω_limit_point x l" unfolding ω_limit_point_def using props(1) r
by (metis comp_assoc)
moreover have "l ∉ A" using s(1) r(3) ‹open A› unfolding tendsto_def by auto
moreover have "l ∉ B" using s(1) r(3) ‹open B› unfolding tendsto_def by auto
ultimately show False using ‹ω_limit_set x ⊆ A ∪ B› unfolding ω_limit_set_def
by auto
qed

lemma ω_limit_set_in_compact_ω_limit_set_contained:
shows "∀y ∈ ω_limit_set x. ω_limit_set y ⊆ ω_limit_set x"
proof safe
fix y z
assume "y ∈ ω_limit_set x" "z ∈ ω_limit_set y"
then have "ω_limit_point y z" unfolding ω_limit_set_def by auto
from ω_limit_pointE[OF this]
obtain s where s: "(flow0 y ∘ s) ⇢ z" .
have "∀n. (flow0 y ∘ s) n ∈ ω_limit_set x"
using ‹y ∈ ω_limit_set x› invariant_def
ω_limit_set_in_compact_existence ω_limit_set_invariant trapped_iff_on_existence_ivl0
by force
thus "z ∈ ω_limit_set x" using closed_sequential_limits s ω_limit_set_closed
by blast
qed

lemma ω_limit_set_in_compact_α_limit_set_contained:
assumes zpx: "z ∈ ω_limit_set x"
shows "α_limit_set z ⊆ ω_limit_set x"
proof
fix w assume "w ∈ α_limit_set z"
then obtain s where s: "(flow0 z ∘ s) ⇢ w"
unfolding α_limit_set_def α_limit_point_def
by auto
from ω_limit_set_invariant have "invariant (ω_limit_set x)" .
then have "∀n. (flow0 z ∘ s) n ∈ ω_limit_set x"
using ω_limit_set_in_compact_existence[OF zpx] zpx
using invariant_def trapped_iff_on_existence_ivl0 by fastforce
from closed_sequentially[OF ω_limit_set_closed this s]
show "w ∈ ω_limit_set x" .
qed

end

text ‹ Fundamental properties of the negative limit set ›

end context auto_ll_on_open begin

context
fixes x K
assumes x: "x ∈ X" "trapped_backward x K"
assumes K: "compact K" "K ⊆ X"
begin

private lemma xrev: "x ∈ X" "rev.trapped_forward x K"
using trapped_backward_iff_rev_trapped_forward x(2)
by (auto simp: rev_existence_ivl_eq0 rev_eq_flow x(1))

lemma α_limit_set_in_compact_subset: "α_limit_set x ⊆ K"
and α_limit_set_in_compact_compact: "compact (α_limit_set x)"
and α_limit_set_in_compact_nonempty: "α_limit_set x ≠ {}"
and α_limit_set_in_compact_connected: "connected (α_limit_set x)"
and α_limit_set_in_compact_α_limit_set_contained:
"∀y ∈ α_limit_set x. α_limit_set y ⊆ α_limit_set x"
and α_limit_set_in_compact_tendsto: "((λt. infdist (flow0 x t) (α_limit_set x)) ⤏ 0) at_bot"
using rev.ω_limit_set_in_compact_subset[OF K xrev]
using rev.ω_limit_set_in_compact_compact[OF K xrev]
using rev.ω_limit_set_in_compact_nonempty[OF K xrev]
using rev.ω_limit_set_in_compact_connected[OF K xrev]
using rev.ω_limit_set_in_compact_ω_limit_set_contained[OF K xrev]
using rev.ω_limit_set_in_compact_tendsto[OF K xrev]
unfolding invariant_eq_rev α_limit_set_eq_rev existence_ivl_eq_rev flow_eq_rev0 filterlim_at_bot_mirror
minus_minus
.

lemma α_limit_set_in_compact_existence:
shows "⋀y. y ∈ α_limit_set x ⟹ existence_ivl0 y = UNIV"
using rev.ω_limit_set_in_compact_existence[OF K xrev]
unfolding α_limit_set_eq_rev existence_ivl_eq_rev0
by auto

end
end

end


# Theory Periodic_Orbit

section ‹Periodic Orbits›
theory Periodic_Orbit
imports
Ordinary_Differential_Equations.ODE_Analysis
Analysis_Misc
ODE_Misc
Limit_Set
begin

text ‹ Definition of closed and periodic orbits and their associated properties ›

context auto_ll_on_open
begin

text ‹
TODO: not sure if the "closed orbit" terminology is standard
Closed orbits have some non-zero recurrence time T where the flow returns to the initial state
The period of a closed orbit is the infimum of all positive recurrence times
Periodic orbits are the subset of closed orbits where the period is non-zero
›

definition "closed_orbit x ⟷
(∃T ∈ existence_ivl0 x. T ≠ 0 ∧ flow0 x T = x)"

definition "period x =
Inf {T ∈ existence_ivl0 x. T > 0 ∧ flow0 x T = x}"

definition "periodic_orbit x ⟷
closed_orbit x ∧ period x > 0"

lemma recurrence_time_flip_sign:
assumes "T ∈ existence_ivl0 x" "flow0 x T = x"
shows "-T ∈ existence_ivl0 x" "flow0 x (-T) = x"
using assms existence_ivl_reverse apply fastforce
using assms flows_reverse by fastforce

lemma closed_orbit_recurrence_times_nonempty:
assumes "closed_orbit x"
shows " {T ∈ existence_ivl0 x. T > 0 ∧ flow0 x T = x} ≠ {}"
apply auto
using assms(1) unfolding closed_orbit_def
by (smt recurrence_time_flip_sign)

lemma closed_orbit_recurrence_times_bdd_below:
shows "bdd_below {T ∈ existence_ivl0 x. T > 0 ∧ flow0 x T = x}"
unfolding bdd_below_def
by (auto) (meson le_cases not_le)

lemma closed_orbit_period_nonneg:
assumes "closed_orbit x"
shows "period x ≥ 0"
unfolding period_def
using assms(1) unfolding closed_orbit_def apply (auto intro!:cInf_greatest)
by (smt recurrence_time_flip_sign)

lemma closed_orbit_in_domain:
assumes "closed_orbit x"
shows "x ∈ X"
using assms unfolding closed_orbit_def
using local.mem_existence_ivl_iv_defined(2) by blast

lemma closed_orbit_global_existence:
assumes "closed_orbit x"
shows "existence_ivl0 x = UNIV"
proof -
obtain Tp where "Tp ≠ 0" "Tp ∈ existence_ivl0 x" "flow0 x Tp = x" using assms
unfolding closed_orbit_def by blast
then obtain T where T: "T > 0" "T ∈ existence_ivl0 x" "flow0 x T = x"
by (smt recurrence_time_flip_sign)
have apos: "real n * T ∈ existence_ivl0 x ∧ flow0 x (real n * T) = x" for n
proof (induction n)
case 0
then show ?case using closed_orbit_in_domain assms by auto
next
case (Suc n)
fix n
assume ih:"real n * T ∈ existence_ivl0 x ∧ flow0 x (real n * T) = x"
then have "T ∈ existence_ivl0 (flow0 x (real n * T))" using T by metis
then have l:"real n * T + T ∈ existence_ivl0 x" using ih
using existence_ivl_trans by blast
have "flow0 (flow0 x (real n * T)) T = x" using ih T by metis
then have r: "flow0 x (real n * T + T) = x"
by (simp add: T(2) ih local.flow_trans)
show "real (Suc n) * T ∈ existence_ivl0 x ∧ flow0 x (real (Suc n) * T) = x"
using l r
qed
then have aneg: "-real n * T ∈ existence_ivl0 x ∧ flow0 x (-real n * T) = x" for n
have "∀t. t ∈ existence_ivl0 x"
proof safe
fix t
have "t ≥ 0 ∨ t ≤ (0::real)" by linarith
moreover {
assume "t ≥ 0"
obtain k where "real k * T > t"
using T(1) ex_less_of_nat_mult by blast
then have "t ∈ existence_ivl0 x" using apos
by (meson ‹0 ≤ t› atLeastAtMost_iff less_eq_real_def local.ivl_subset_existence_ivl subset_eq)
}
moreover {
assume "t ≤ 0"
obtain k where "- real k * T < t"
by (metis T(1) add.inverse_inverse ex_less_of_nat_mult mult.commute mult_minus_right neg_less_iff_less)
then have "t ∈ existence_ivl0 x" using aneg
by (smt apos atLeastAtMost_iff calculation(2) local.existence_ivl_trans' local.ivl_subset_existence_ivl mult_minus_left subset_eq)
}
ultimately show "t ∈ existence_ivl0 x" by blast
qed
thus ?thesis by auto
qed

lemma recurrence_time_multiples:
fixes n::nat
assumes "T ∈ existence_ivl0 x" "T ≠ 0" "flow0 x T = x"
shows "⋀t. flow0 x (t+T*n) = flow0 x t"
proof (induction n)
case 0
then show ?case by auto
next
case (Suc n)
fix n t
assume ih : "(⋀t. flow0 x (t + T * real n) = flow0 x t)"
have "closed_orbit x" using assms unfolding closed_orbit_def by auto
from closed_orbit_global_existence[OF this] have ex:"existence_ivl0 x = UNIV" .
have "flow0 x (t + T * real (Suc n)) = flow0 x (t+T*real n + T)"
also have "... = flow0 (flow0 x (t+ T*real n)) T" using ex
also have "... = flow0 (flow0 x t) T" using ih by auto
also have "... = flow0 (flow0 x T) t" using ex
by (metis UNIV_I add.commute local.existence_ivl_trans' local.flow_trans)
finally show "flow0 x (t + T * real (Suc n)) = flow0 x t" using assms(3) by simp
qed

lemma nasty_arithmetic1:
fixes t T::real
assumes "T > 0" "t ≥ 0"
obtains q r where "t = (q::nat) * T + r" "0 ≤ r" "r < T"
proof -
define q where "q = floor (t / T)"
have q:"q ≥ 0" using assms unfolding q_def by auto
from floor_divide_lower[OF assms(1), of t]
have ql: "q * T ≤ t" unfolding q_def .
from floor_divide_upper[OF assms(1), of t]
have qu: "t < (q + 1)* T" unfolding q_def by auto
define r where "r = t - q * T"
have rl:"0 ≤ r" using ql unfolding r_def by auto
have ru:"r < T" using qu unfolding r_def  by (simp add: distrib_right)
show ?thesis using q r_def rl ru
qed

lemma nasty_arithmetic2:
fixes t T::real
assumes "T > 0" "t ≤ 0"
obtains q r where "t = (q::nat) * (-T) + r" "0 ≤ r" "r < T"
proof -
have "-t ≥ 0" using assms(2) by linarith
from nasty_arithmetic1[OF assms(1) this]
obtain q r where qr: "-t = (q::nat) * T + r" "0 ≤ r" "r < T" by blast
then have "t = q * (-T) - r"  by auto
then have "t = (q+(1::nat)) * (-T) + (T-r)" by (simp add: distrib_right)
thus ?thesis using qr(2-3)
by (smt ‹t = real q * - T - r› that)
qed

lemma recurrence_time_restricts_compact_flow:
assumes "T ∈ existence_ivl0 x" "T > 0" "flow0 x T = x"
shows "flow0 x  UNIV = flow0 x  {0..T}"
apply auto
proof -
fix t
have "t ≥ 0 ∨ t ≤ (0::real)" by linarith
moreover {
assume "t ≥ 0"
from nasty_arithmetic1[OF assms(2) this]
obtain q r where qr:"t = (q::nat) * T + r" "0 ≤ r" "r < T" by blast
have "T ≠ 0" using assms(2) by auto
from recurrence_time_multiples[OF assms(1) this assms(3),of "r" "q"]
have "flow0 x t = flow0 x r"
then have "flow0 x t ∈ flow0 x  {0..<T}" using qr by auto
}
moreover {
assume "t ≤ 0"
from nasty_arithmetic2[OF assms(2) this]
obtain q r where qr:"t = (q::nat) * (-T) + r" "0 ≤ r" "r < T" by blast
have "-T ∈ existence_ivl0 x" "-T ≠ 0" "flow0 x (-T) = x" using recurrence_time_flip_sign assms by auto
from recurrence_time_multiples[OF this, of r q]
have "flow0 x t = flow0 x r"
then have "flow0 x t ∈ flow0 x  {0..<T}" using qr by auto
}
ultimately show "flow0 x t ∈ flow0 x  {0..T}"
by auto
qed

lemma closed_orbitI:
assumes "t ≠ t'" "t ∈ existence_ivl0 y" "t' ∈ existence_ivl0 y"
assumes "flow0 y t = flow0 y t'"
shows "closed_orbit y"
unfolding closed_orbit_def
by (smt assms local.existence_ivl_reverse local.existence_ivl_trans local.flow_trans local.flows_reverse)

(* TODO: can be considerably generalized *)
lemma flow0_image_UNIV:
assumes "existence_ivl0 x = UNIV"
shows "flow0 (flow0 x t)  S = flow0 x  (λs. s + t)  S"
apply auto
apply (metis UNIV_I add.commute assms image_eqI local.existence_ivl_trans' local.flow_trans)
by (metis UNIV_I add.commute assms imageI local.existence_ivl_trans' local.flow_trans)

lemma recurrence_time_restricts_compact_flow':
assumes "t < t'" "t ∈ existence_ivl0 y" "t' ∈ existence_ivl0 y"
assumes "flow0 y t = flow0 y t'"
shows "flow0 y  UNIV = flow0 y  {t..t'}"
proof -
have "closed_orbit y"
using assms(1-4) closed_orbitI inf.strict_order_iff by blast
from closed_orbit_global_existence[OF this]
have yex: "existence_ivl0 y = UNIV" .
have a1:"t'- t ∈ existence_ivl0 (flow0 y t)"
have a2:"t' -t > 0" using assms(1) by auto
have a3:"flow0 (flow0 y t) (t' - t) = flow0 y t"
using a1 assms(2) assms(4) local.flow_trans by fastforce
from recurrence_time_restricts_compact_flow[OF a1 a2 a3]
have eq:"flow0 (flow0 y t)  UNIV = flow0 (flow0 y t)  {0.. t'-t}" .
from flow0_image_UNIV[OF yex, of _ "UNIV"]
have eql:"flow0 (flow0 y t)  UNIV = flow0 y  UNIV"
by (metis (no_types) add.commute surj_def surj_plus)
from flow0_image_UNIV[OF yex, of _ "{0..t'-t}"]
have eqr:"flow0 (flow0 y t)  {0.. t'-t} = flow0 y  {t..t'}" by auto
show ?thesis using eq eql eqr by auto
qed

lemma closed_orbitE':
assumes "closed_orbit x"
obtains T where "T > 0" "⋀t (n::nat). flow0 x (t+T*n) = flow0 x t"
proof -
obtain Tp where "Tp ≠ 0" "Tp ∈ existence_ivl0 x" "flow0 x Tp = x" using assms
unfolding closed_orbit_def by blast
then obtain T where T: "T > 0" "T ∈ existence_ivl0 x" "flow0 x T = x"
by (smt recurrence_time_flip_sign)
thus ?thesis using  recurrence_time_multiples T that by blast
qed

lemma closed_orbitE:
assumes "closed_orbit x"
obtains T where "T > 0" "⋀t. flow0 x (t+T) = flow0 x t"
using closed_orbitE'
by (metis assms mult.commute reals_Archimedean3)

lemma closed_orbit_flow_compact:
assumes "closed_orbit x"
shows "compact(flow0 x  UNIV)"
proof -
obtain Tp where "Tp ≠ 0" "Tp ∈ existence_ivl0 x" "flow0 x Tp = x" using assms
unfolding closed_orbit_def by blast
then obtain T where T: "T ∈ existence_ivl0 x" "T > 0" "flow0 x T = x"
by (smt recurrence_time_flip_sign)
from recurrence_time_restricts_compact_flow[OF this]
have feq: "flow0 x  UNIV = flow0 x  {0..T}" .
have "continuous_on {0..T} (flow0 x)"
by (meson T(1) continuous_on_sequentially in_mono local.flow_continuous_on local.ivl_subset_existence_ivl)
from compact_continuous_image[OF this]
have "compact (flow0 x  {0..T})" by auto
thus ?thesis using feq by auto
qed

lemma fixed_point_imp_closed_orbit_period_zero:
assumes "x ∈ X"
assumes "f x = 0"
shows "closed_orbit x" "period x = 0"
proof -
from fixpoint_sol[OF assms] have fp:"existence_ivl0 x = UNIV" "⋀t. flow0 x t = x" by auto
then have co:"closed_orbit x" unfolding closed_orbit_def by blast
have a: "∀y>0. ∃a∈{T ∈ existence_ivl0 x. 0 < T ∧ flow0 x T = x}. a < y"
apply auto
using fp
from cInf_le_iff[OF closed_orbit_recurrence_times_nonempty[OF co]
closed_orbit_recurrence_times_bdd_below , of 0]
have "period x ≤ 0" unfolding period_def using a by auto
from closed_orbit_period_nonneg[OF co] have "period x ≥ 0" .
then have "period x = 0" using ‹period x ≤ 0› by linarith
thus "closed_orbit x" "period x = 0" using co by auto
qed

lemma closed_orbit_period_zero_fixed_point:
assumes "closed_orbit x" "period x = 0"
shows "f x = 0"
proof (rule ccontr)
assume "f x ≠ 0"
from regular_locally_noteq[OF closed_orbit_in_domain[OF assms(1)] this]
have "∀⇩F t in at 0. flow0 x t ≠ x " .
then obtain r where "r>0" "∀t. t ≠ 0 ∧ dist t 0 < r ⟶ flow0 x t ≠ x" unfolding eventually_at
by auto
then have "period x ≥ r" unfolding period_def
apply (auto intro!:cInf_greatest)
apply (meson assms(1) closed_orbit_def linorder_neqE_linordered_idom neg_0_less_iff_less recurrence_time_flip_sign)
using not_le by force
thus False using assms(2) ‹r >0› by linarith
qed

lemma closed_orbit_subset_ω_limit_set:
assumes "closed_orbit x"
shows "flow0 x  UNIV ⊆ ω_limit_set x"
unfolding ω_limit_set_def ω_limit_point_def
proof clarsimp
fix t
from closed_orbitE'[OF assms]
obtain T where T: "0 < T" "⋀t n. flow0 x (t + T* real n) = flow0 x t" by blast
define s where "s = (λn::nat. t + T * real n)"
have exist: "{0..} ⊆ existence_ivl0 x"
have l:"filterlim s at_top sequentially" unfolding s_def
using T(1)
have "flow0 x ∘ s = (λn. flow0 x t)" unfolding o_def s_def using T(2) by simp
then have r:"(flow0 x ∘ s) ⇢ flow0 x t" by auto
show "{0..} ⊆ existence_ivl0 x ∧ (∃s. s ⇢⇘⇙ ∞ ∧ (flow0 x ∘ s) ⇢ flow0 x t)"
using exist l r by blast
qed

lemma closed_orbit_ω_limit_set:
assumes "closed_orbit x"
shows "flow0 x  UNIV = ω_limit_set x"
proof -
have "ω_limit_set x ⊆ flow0 x  UNIV"
using closed_orbit_global_existence[OF assms]
by (intro ω_limit_set_in_compact_subset)
(auto intro!: flow_in_domain
simp add: assms closed_orbit_in_domain image_subset_iff trapped_forward_def
closed_orbit_flow_compact)
thus ?thesis using closed_orbit_subset_ω_limit_set[OF assms] by auto
qed

lemma flow0_inj_on:
assumes "t ≤ t'"
assumes "{t..t'} ⊆ existence_ivl0 x"
assumes "⋀s. t < s ⟹ s ≤ t' ⟹ flow0 x s ≠ flow0 x t"
shows "inj_on (flow0 x) {t..t'}"
apply (rule inj_onI)
proof (rule ccontr)
fix u v
assume uv: "u ∈ {t..t'}" "v ∈ {t..t'}" "flow0 x u = flow0 x v" "u ≠ v"
have "u < v ∨ v < u" using uv(4) by linarith
moreover {
assume "u < v"
from recurrence_time_restricts_compact_flow'[OF this _ _ uv(3)]
have "flow0 x  UNIV = flow0 x  {u..v}"  using uv(1-2) assms(2) by blast
then have "flow0 x t ∈ flow0 x  {u..v}" by auto
moreover have "u = t ∨ flow0 x t ∉ flow0 x  {u..v}" using assms(3)
by (smt atLeastAtMost_iff image_iff uv(1) uv(2))
ultimately have False using uv assms(3)
by force
}
moreover {
assume "v < u"
from recurrence_time_restricts_compact_flow'[OF this _ _ ]
have "flow0 x  UNIV = flow0 x  {v..u}"
by (metis assms(2) subset_iff uv(1) uv(2) uv(3))
then have "flow0 x t ∈ flow0 x  {v..u}" by auto
moreover have "v `