Session Poincare_Bendixson

Theory Analysis_Misc

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

subsection ‹Unsorted Lemmas (TODO: sort!)›

lemma uminus_uminus_image: "uminus ` uminus ` S = S"
  for S::"'r::ab_group_add set"
  by (auto simp: image_image)

lemma in_uminus_image_iff[simp]: "x  uminus ` S  - x  S"
  for S::"'r::ab_group_add set"
  by force

lemma closed_subsegmentI:
  "w + t *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}
  for g::"_  'b::topological_group_add"
  by (simp add: tendsto_minus_cancel_left)

lemma tendsto_nhds_continuousI: "(f  l) (nhds x)" if "(f  l) (at x)" "f x = l"
  ― ‹TODO: the assumption is continuity of f at x›
proof (rule topological_tendstoI)
  fix S::"'b set" assume "open S" "l  S"
  from topological_tendstoD[OF that(1) this]
  have "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
  by atomize_elim (simp add: infinite_countable_subset)

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

lemma inner_quad_ge: "2 * (a  b)  a  a + b  b"
  for a b::"'a::euclidean_space"― ‹generalize?›
proof -
  show ?thesis
    by (subst (1 2 3) euclidean_inner)
      (auto simp add: sum.distrib[symmetric] sum_distrib_left intro!: sum_mono real_quad_ge)
qed

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

lemma closed_segment_line_hyperplanes:
  "{a -- b} = range (λu. a + u *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"
    by (rule inner_quad_ge)
  then have "u * (2 * (a  b) - a  a - b  b)  0"
    "0  (1 - u) * (a  a + b  b - a  b * 2)"
    by (simp_all add: mult_le_0_iff u)
  then show " a  (b - a)  x  (b - a)" "x  (b - a)  b  (b - a)"
    by (auto simp: x_eq algebra_simps power2_eq_square inner_commute)
next
  fix u assume
    "a  (b - a)  (a + u *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
    by (auto simp add: zero_le_mult_iff)
  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
    by (rule inner_quad_gt)
  then have "u * (2 * (a  b) - a  a - b  b) < 0"
    "0 < (1 - u) * (a  a + b  b - a  b * 2)"
    by (simp_all add: mult_less_0_iff u)
  then show " a  (b - a) < x  (b - a)" "x  (b - a) < b  (b - a)"
    by (auto simp: x_eq algebra_simps power2_eq_square inner_commute)
next
  fix u assume
    "a  (b - a) < (a + u *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
    by (auto simp add: zero_less_mult_iff)
  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
    by (metis (full_types) add.commute trans_le_add2)
  from LIMSEQ_ignore_initial_segment[OF assms(2), of "k"]
  have "(λn. (f  s) (n + k))  l" .
  then have "(f  t)  l" unfolding t_def o_def by simp
  show ?thesis
    using (f  t)  l n. b  t n ‹filterlim t at_top sequentially› that by blast
qed

lemma frequently_at_top_realE:
  fixes P::"nat  real  bool"
  assumes "n. 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})"
  by (auto intro!:closed_Collect_le simp add:continuous_on_infdist)

(* TODO: this is a copy of LIMSEQ_norm_0 where the sequence
  is bounded above in norm by a geometric series *)
lemma LIMSEQ_norm_0_pow:
  assumes "k > 0" "b > 1"
  assumes  "n::nat. norm (s n)  k / b^n"
  shows "s  0"
proof (rule metric_LIMSEQ_I)
  fix e
  assume "e > (0::real)"
  then have "k / e > 0" using assms(1) by auto
  obtain N where N: "b^(N::nat) > k / e" using assms(2)
    using 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)
        (metis add.commute add_divide_distrib diff_add_cancel scaleR_add_left)
    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)"
  by (simp add: line_def algebra_simps)

lemma line_line2: "line a (line a b c) x = line a b (c*x)"
  by (simp add: line_def algebra_simps)

lemma line_in_subsegment:
  "i1 < 1  i2 < 1  a  b  line a b i1  {line a b i2<--<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
    by (auto simp: add_nonneg_pos pos_add_strict)
  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)
      (metis uv add_less_same_cancel1 add_strict_mono mult.right_neutral
        mult_less_cancel_left_pos not_real_square_gt_zero vector_space_over_itself.scale_zero_left)
  then have "(ua * (u * v - u - v) - - u) *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)"
    by (simp add: right_diff_distrib')
  have f2: "r ra. (r::real) - r * ra = r * (1 - ra)"
    by (simp add: right_diff_distrib')
  have f3: "r ra rb. (r::real) - ra + rb + ra - r = rb"
    by auto
  have f4: "r. (r::real) + (1 - 1) = r"
    by linarith
  have f5: "r ra. (r::real) + ra = ra + r"
    by force
  have f6: "r ra. (r::real) + (1 - (r + 1) + ra) = ra"
    by linarith
  have "t - x * (t - (t + u * (t' - t))) = t' * (u * x) + (t - t * (u * x))"
    by (simp add: right_diff_distrib')
  then show "(1 - u * x) * t + u * x * t' = (1 - x) * t + x * (t + u * (t' - t))"
    using f6 f5 f4 f3 f2 f1 by (metis (no_types) mult.commute)
qed

lemma linepath_image0_right_open_real:
  assumes "t < (t'::real)"
  shows "linepath t t' ` {0..<1} = {t..<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
      by (simp add: mult.commute)
  qed
  ultimately show "x  (λx. (1 - x) * t + x * t') ` {0..<1}"
    using atLeastLessThan_iff by blast 
qed

lemma oriented_subsegment_scale:
  assumes "x1  {a<--<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
    by (metis add.commute add_diff_cancel_right diff_minus_eq_add scaleR_collapse scaleR_left.minus)
  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 )"
    by (smt add_diff_cancel diff_diff_add diff_minus_eq_add minus_diff_eq scaleR_collapse scale_minus_left scale_right_diff_distrib)
  finally have x2x1:"x2-x1 = (v *(1-u)) *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))"
        by (simp add: dist_real_def)
      also have "  L * dist (φ x) (ψ x)"
        using x  {a .. b}
        by (rule L)
      also have "  -L * w x"
        using 0 < L a0 that
        by (force simp add: dist_real_def abs_real_def w_def algebra_split_simps )
      finally show ?thesis
        by simp
    qed
    have mono: "mono_on (λ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)"])
   apply (simp add: has_derivative_mult_right mult_commute_abs)
  by (auto intro!: continuous_intros)

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

subsection ‹Locally Lipschitz ODEs›

context ll_on_open_it begin

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

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

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

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

lemmas existence_ivl_undefined = existence_ivl_empty2

end

subsection ‹Reverse flow as Sublocale›

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

context auto_ll_on_open begin

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

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

lemma rev_existence_ivl_eq0: "rev.existence_ivl0 y = uminus ` existence_ivl0 y" for y
  using uminus_uminus_image[of "rev.existence_ivl0 y"]
  by (simp add: existence_ivl_eq_rev0)

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

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

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

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

end

context c1_on_open begin

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

end

context c1_on_open_euclidean begin

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

end


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

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

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

context auto_ll_on_open begin

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

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

lemma open_existence_ivl_on_compact:
  assumes C: "C  X" and "compact C" "C  {}"
  obtains a where "a > 0" "x. x  C  {-a..a}  existence_ivl0 x"
proof -
  from existence_ivl_cballs
  have "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"
    by (simp add: assms(3) local.flow_in_domain)
  from trapped_sol_right[OF assms(1-2) xtk assms(4)] have "{0..}  existence_ivl0 (flow0 x t)" .
  thus "{t..}  existence_ivl0 x"
    using existence_ivl_trans[OF assms(3)]
    by (metis add.commute atLeast_iff diff_add_cancel le_add_same_cancel1 subset_iff)
qed

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

lemma trapped_sol_left_gen:
  assumes "compact K" "K  X"
  assumes "t  existence_ivl0 x" "trapped_backward (flow0 x t) K"
  shows "{..t}  existence_ivl0 x"
proof -
  have "x  X"
    using assms(3) local.existence_ivl_empty_iff by fastforce 
  have xtk: "flow0 x t  X"
    by (simp add: assms(3) local.flow_in_domain)
  from trapped_sol_left[OF assms(1-2) xtk assms(4)] have "{..0}  existence_ivl0 (flow0 x t)" .
  thus "{..t}  existence_ivl0 x"
    using existence_ivl_trans[OF assms(3)]
    by (metis add.commute add_le_same_cancel1 atMost_iff diff_add_cancel subset_eq)
qed

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

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

lemma compact_max_time_flow_in_closed:
  assumes "closed M" and t_ex: "t  existence_ivl0 x"
  shows "compact {s  {0..t}. flow0 x ` {0..s}  M}" (is "compact ?C")
  unfolding compact_eq_bounded_closed
proof
  have "bounded {0 .. t}" by auto
  then show "bounded ?C"
    by (rule bounded_subset) auto
  show "closed ?C"
    unfolding closed_def
  proof (rule topological_space_class.openI, clarsimp)
    ― ‹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)"
    by (simp add: poincare_map_def)
  have "return_time {x  S. s x = 0} x  existence_ivl0 x"
    "x  X"
    "s (poincare_map ?P x) = 0"
    using poincare_map_returns rt
    by (auto intro!: return_time_exivl rt)
  note E = flow_implicit_function[of "return_time ?P x" x s Ds, OF this[unfolded *] Ds[unfolded *],
      folded *]
  show ?thesis
    by (rule E) rule
qed

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

lemma flow_transversal_surface_finite_intersections:
  fixes s::"'a  'b::real_normed_vector"
    and Ds::"'a  'a L 'b"
  assumes "closed S"
  assumes "x. (s has_derivative (Ds x)) (at x)"
  assumes "x. x  S  s x = 0  Ds x (f x)  0"
  assumes "a  b" "{a .. b}  existence_ivl0 x"
  shows "finite {t{a..b}. flow0 x t  {x  S. s x = 0}}"
    ― ‹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 by (simp add: blinfun.bilinear_simps)
        subgoal
          apply (rule divide_left_mono)
          using lipschitz_onD[OF L, of "t n" tl] 0 < L t(3) tl(2)
          by (auto simp: algebra_split_simps zero_less_divide_iff dist_norm pos_divide_le_eq
              intro!: add_pos_nonneg)
        done
      done
    ultimately have "Ds (flow0 x tl) (f (flow0 x tl)) = 0"
      by (rule LIMSEQ_unique)
    moreover have "Ds (flow0 x tl) (f (flow0 x tl))  0"
      by (rule transversal) (use ‹flow0 x tl  ?S in auto)
    ultimately show False by auto
  qed
qed (use assms in auto)

lemma uniform_limit_flow0_state:― ‹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"
      by (simp add: eventually_ball_finite_distrib)
    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 (simp add: c'(2))
        apply (drule bspec) prefer 2 apply assumption
        apply auto
        using c'(1) by auto
      done
  qed
qed

end

subsection ‹Fixpoints›

context auto_ll_on_open begin

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

end

end

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
  by (simp add: rev.trapped_backward_iff_rev_trapped_forward)

lemma negatively_invariant_eq_rev: "negatively_invariant M = rev.positively_invariant M"
  unfolding negatively_invariant_def rev.positively_invariant_def
  by (simp add: trapped_backward_iff_rev_trapped_forward)

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
    by (simp add: negatively_invariant_eq_rev)
  then have "rev.negatively_invariant (X-(X-M))"
    by (simp add: rev.negatively_invariant_complI)
  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)"
  by (simp add: invariant_iff_pos_and_neg_invariant neg_invariant_iff_compl_pos_invariant)

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"
    by (simp add: local.ivl_subset_existence_ivl)
  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))"
    apply (auto simp add:o_def has_field_derivative_def)
  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"
    by (simp add: t(2))
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)"
      by (simp add: power2_eq_square)
  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
  by (simp add: assms)

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

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

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

end context auto_ll_on_open begin

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

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

lemma α_limit_set_positively_invariant:
  shows "negatively_invariant (α_limit_set x)"
  unfolding negatively_invariant_eq_rev α_limit_set_eq_rev
  by (simp add: rev.ω_limit_set_positively_invariant)

lemma α_limit_set_invariant:
  shows "invariant (α_limit_set x)"
  unfolding invariant_eq_rev α_limit_set_eq_rev
  by (simp add: rev.ω_limit_set_invariant)

text ‹ Fundamental properties of the positive limit set ›

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

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

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

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

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

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

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

lemma ω_limit_set_in_compact_tendsto:
  shows "((λt. infdist (flow0 x t) (ω_limit_set x))  0) at_top"
proof (rule ccontr)
  assume "¬ ((λt. infdist (flow0 x t) (ω_limit_set x))  0) at_top"
  from not_tendsto_frequentlyE[OF this]
  obtain S where S: "open S" "0  S"
    "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
      by (simp add: add.commute distrib_left mult.commute)
  qed
  then have aneg: "-real n * T  existence_ivl0 x  flow0 x (-real n * T) = x" for n
    by (simp add: recurrence_time_flip_sign)
  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)"
    by (simp add: Groups.add_ac(3) add.commute distrib_left)
  also have "... = flow0 (flow0 x (t+ T*real n)) T" using ex
    by (simp add: local.existence_ivl_trans' local.flow_trans)
  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
    by (metis le_add_diff_inverse of_int_of_nat_eq plus_int_code(2) ql that zle_iff_zadd)
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"
      by (simp add: qr(1) add.commute mult.commute)
    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"
      by (simp add: mult.commute qr(1))
    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)"
    by (simp add: assms(2-3) local.existence_ivl_trans')
  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
    by (simp add: dense) 
  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"
    by (simp add: assms closed_orbit_global_existence)
  have l:"filterlim s at_top sequentially" unfolding s_def
    using T(1)
    by (auto intro!:filterlim_tendsto_add_at_top filterlim_tendsto_pos_mult_at_top
        simp add: filterlim_real_sequentially)
  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