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 (z3) 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 "a∙i" "b∙i"]
    by (auto intro!: le_neq_trans real_quad_ge)
  then show ?thesis
    by (subst (1 2 3) euclidean_inner)
      (auto simp add: ‹i ∈ Basis› sum.distrib[symmetric] sum_distrib_left
        intro!: sum_strict_mono_ex1 real_quad_ge)
qed

lemma closed_segment_line_hyperplanes:
  "{a -- b} = range (λu. a + u *⇩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. ∀x≥x0. dist (f x) l < e"
for f::"'a::linorder_topology ⇒ 'b::metric_space"
  using that
  apply (intro tendstoI)
  unfolding eventually_at_top_linorder
  by auto

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

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

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

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

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

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

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

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

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


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

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

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

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

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

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

context linorder
begin

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

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

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

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

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

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

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

end

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(* Used to sharpen a tendsto with additional information*)
lemma filterlim_at_top_choose_lower:
  assumes "filterlim s at_top sequentially"
  assumes "(f ∘ s) ⇢ l"
  obtains t where
    "filterlim t at_top sequentially"
    "(f ∘ t) ⇢ l"
    "∀n. t n ≥ (b::real)"
proof -
  obtain k where k: "∀n ≥ k. s n ≥ b" using assms(1)
    unfolding filterlim_at_top eventually_sequentially by blast
  define t where "t = (λn. s (n+k))"
  then have "∀n. t n ≥ b" using k by simp
  have "filterlim t at_top sequentially" using assms(1)
    unfolding filterlim_at_top eventually_sequentially t_def
    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::"nat⇒real"
  where "⋀i. P i (s i)" "filterlim s at_top at_top"
  by (metis assms frequently_at_top_at_topE[OF _ filterlim_real_sequentially])

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

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

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

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

lemma infdist_closed:
  shows "closed ({z. infdist z S ≥ e})"
  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 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 (z3) assms(1) assms(2) frac_le leD power_less_imp_less_exp that zero_less_power)
    also have " ... < e" using N
      by (metis ‹0 < e› assms(2) less_trans mult.commute pos_divide_less_eq zero_less_one zero_less_power)
    finally show ?thesis
      by (meson assms less_eq_real_def not_le order_trans)
  qed
  then show "∃no. ∀n≥no. dist (s n) 0 < e"
    by auto
qed

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

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

subsection ‹indexing euclidean space with natural numbers›

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

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

open_bundle eucl_syntax
begin
notation nth_eucl (infixl ‹$⇩e› 90)
end

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
  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
  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::"(nat⇒real)⇒bool"
  (‹_ ⇢⇘⇙ ∞›) ― ‹the ‹⇘⇙› is to disambiguate syntax...›
  where "s ⇢⇘⇙ ∞  ≡ filterlim s at_top sequentially"

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


subsection ‹Paths›

lemma subpath0_linepath:
  shows "subpath 0 u (linepath t t') = linepath t (t + u * (t' - t))"
  unfolding subpath_def linepath_def
  apply (rule ext)
  apply auto
proof -
  fix x :: real
  have f1: "⋀r ra rb rc. (r::real) + ra * rb - ra * rc = r - ra * (rc - rb)"
    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 (z3) 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 (z3) field_class.field_inverse scaleR_one scaleR_scaleR) 
  thus ?thesis
    using ‹0 < v * (1 - u)› positive_imp_inverse_positive that by fastforce
qed

end