Theory Analysis_Misc

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 "ai" "bi"]
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. xx0. 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. xx0. 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  (xS. 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 "tT. 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. nn0. s n < u"
proof -
from fl have "no>0. nno. 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::"natreal"
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  ttt. 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. nno. 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::natreal) = (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::"(natreal)bool"
("_  ") ― ‹the  is to disambiguate syntax...›
where "s    filterlim s at_top sequentially"

abbreviation sequentially_at_bot::"(natreal)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 "xC. e>0. t>0. ycball x e. cball 0 texistence_ivl0 y"
by (metis (full_types) C Int_absorb1 Int_iff UNIV_I)
then
obtain d' t' where *:
"xC. 0 < d' x  t' x > 0  (ycball 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  (cC'. 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 "us") 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)))) oL
(Ds (flow0 x t) oL flowderiv x t) oL 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)) oL (flowderiv (fst x) (snd x))))
(at x))"
by (auto intro!: derivative_eq_intros)
have C: "isCont (λx. Ds (flow0 (fst x) (snd x)) oL 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)))) oL
((Ds (flow0 (fst (x, t))
(snd (x, t))) oL
flowderiv (fst (x, t))
(snd (x, t))) oL
embed2_blinfun)
= 1L"
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))) oL
flowderiv (fst (x, t))
(snd (x, t))) oL
embed2_blinfun) oL blinfun_scaleR_left (inverse (Ds (flow0 x t)(f (flow0 x t))))
= 1L"
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))) oL (Ds x oL flowderiv x 0) oL 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)))) oL
(Ds (poincare_map ?P x) oL flowderiv x (return_time ?P x)) oL 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 "xC. 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  (cC. 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  (cC'. 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. xball 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 "xball 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. cC'. xball c (u' c). dist (flow0 x s) (flow0 x 0) < e"
then show "F s in at 0. xC. 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  (xM. trapped x M)"

definition "positively_invariant M  (xM. trapped_forward x M)"

definition "negatively_invariant M  (xM. trapped_backward x M)"

lemma positively_invariant_iff:
"positively_invariant M
(xM. flow0 x  (existence_ivl0 x  {0..}))  M"
unfolding positively_invariant_def trapped_forward_def
by auto

lemma negatively_invariant_iff:
"negatively_invariant M
(xM. 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  (xM. 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[1]
using exist  by auto
have cont: "continuous_on dom (λx. flow0 x t)"
apply (rule flow_continuous_on_compose)
apply auto
using p  X  exist local.dom_def local.flow_in_domain apply auto[1]
using xt .
then have f1: "((λx. flow0 x t)  (flow0 x  s))  flow0 p t" using domin s(2)
unfolding continuous_on_sequentially
by blast
have ff:"n. (flow0 x  r) n = ((λx. flow0 x t)  (flow0 x  s)) n"
unfolding o_def r_def
proof -
fix n
have s:"s n  existence_ivl0 x"
using s(3) exist by auto
then have t:"t  existence_ivl0 (flow0 x (s n))"
using domin(1) xt by auto
from flow_trans[OF s t]
show "flow0 x (t + s n) = flow0 (flow0 x (s n)) t"
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[1]
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