Theory Limits

theory Limits
  imports
    HOL.Real_Vector_Spaces
    Zip_Benchmarks_Setup
begin

text ‹Note: this benchmark file is an adjusted copy of HOL.Limits from the standard distribution
(dated 07.11.2025)›

lemma range_mult [simp]:
  fixes a::"real" shows "range ((*) a) = (if a=0 then {0} else UNIV)"
  by (simp add: surj_def) (meson dvdE dvd_field_iff)

subsection ‹Filter going to infinity norm›

definition at_infinity :: "'a::real_normed_vector filter"
  where "at_infinity = (INF r. principal {x. r ≤ norm x})"

lemma eventually_at_infinity: "eventually P at_infinity ⟷ (∃b. ∀x. b ≤ norm x ⟶ P x)"
  unfolding at_infinity_def
  by (subst eventually_INF_base)
     (auto simp: subset_eq eventually_principal intro!: exI[of _ "max a b" for a b])

lemma eventually_at_infinityI:
  fixes P::"'a::real_normed_vector ⇒ bool"
  assumes "⋀x. c ≤ norm x ⟹ P x"
  shows "eventually P at_infinity"
unfolding eventually_at_infinity using assms by auto

corollary eventually_at_infinity_pos:
  "eventually p at_infinity ⟷ (∃b. 0 < b ∧ (∀x. norm x ≥ b ⟶ p x))"
  unfolding eventually_at_infinity
  by (meson le_less_trans norm_ge_zero not_le zero_less_one)

lemma at_infinity_eq_at_top_bot: "(at_infinity :: real filter) = sup at_top at_bot"
proof -
  have 1: "⟦∀n≥u. A n; ∀n≤v. A n⟧
       ⟹ ∃b. ∀x. b ≤ ¦x¦ ⟶ A x" for A and u v::real
    by (rule_tac x="max (- v) u" in exI) (auto simp: abs_real_def)
  have 2: "∀x. u ≤ ¦x¦ ⟶ A x ⟹ ∃N. ∀n≥N. A n" for A and u::real
    by (meson abs_less_iff le_cases less_le_not_le)
  have 3: "∀x. u ≤ ¦x¦ ⟶ A x ⟹ ∃N. ∀n≤N. A n" for A and u::real
    by (metis (full_types) abs_ge_self abs_minus_cancel le_minus_iff order_trans)
  show ?thesis
    by (auto simp: filter_eq_iff eventually_sup eventually_at_infinity
      eventually_at_top_linorder eventually_at_bot_linorder intro: 1 2 3)
qed

lemma at_top_le_at_infinity: "at_top ≤ (at_infinity :: real filter)"
  unfolding at_infinity_eq_at_top_bot by simp

lemma at_bot_le_at_infinity: "at_bot ≤ (at_infinity :: real filter)"
  unfolding at_infinity_eq_at_top_bot by simp

lemma filterlim_at_top_imp_at_infinity: "filterlim f at_top F ⟹ filterlim f at_infinity F"
  for f :: "_ ⇒ real"
  by (rule filterlim_mono[OF _ at_top_le_at_infinity order_refl])

lemma filterlim_real_at_infinity_sequentially: "filterlim real at_infinity sequentially"
  by (simp add: filterlim_at_top_imp_at_infinity filterlim_real_sequentially)

lemma lim_infinity_imp_sequentially: "(f ⤏ l) at_infinity ⟹ ((λn. f(n)) ⤏ l) sequentially"
  by (simp add: filterlim_at_top_imp_at_infinity filterlim_compose filterlim_real_sequentially)


subsubsection ‹Boundedness›

definition Bfun :: "('a ⇒ 'b::metric_space) ⇒ 'a filter ⇒ bool"
  where Bfun_metric_def: "Bfun f F = (∃y. ∃K>0. eventually (λx. dist (f x) y ≤ K) F)"

abbreviation Bseq :: "(nat ⇒ 'a::metric_space) ⇒ bool"
  where "Bseq X ≡ Bfun X sequentially"

lemma Bseq_conv_Bfun: "Bseq X ⟷ Bfun X sequentially" ..

lemma Bseq_ignore_initial_segment: "Bseq X ⟹ Bseq (λn. X (n + k))"
  unfolding Bfun_metric_def by (subst eventually_sequentially_seg)

lemma Bseq_offset: "Bseq (λn. X (n + k)) ⟹ Bseq X"
  unfolding Bfun_metric_def by (subst (asm) eventually_sequentially_seg)

lemma Bfun_def: "Bfun f F ⟷ (∃K>0. eventually (λx. norm (f x) ≤ K) F)"
  unfolding Bfun_metric_def norm_conv_dist
proof safe
  fix y K
  assume K: "0 < K" and *: "eventually (λx. dist (f x) y ≤ K) F"
  moreover have "eventually (λx. dist (f x) 0 ≤ dist (f x) y + dist 0 y) F"
    by (intro always_eventually) (metis dist_commute dist_triangle)
  with * have "eventually (λx. dist (f x) 0 ≤ K + dist 0 y) F"
    by eventually_elim auto
  with ‹0 < K› show "∃K>0. eventually (λx. dist (f x) 0 ≤ K) F"
    by (intro exI[of _ "K + dist 0 y"] add_pos_nonneg conjI zero_le_dist) auto
qed (force simp del: norm_conv_dist [symmetric])

lemma BfunI:
  assumes K: "eventually (λx. norm (f x) ≤ K) F"
  shows "Bfun f F"
  unfolding Bfun_def
proof (intro exI conjI allI)
  show "0 < max K 1" by simp
  show "eventually (λx. norm (f x) ≤ max K 1) F"
    using K by (rule eventually_mono) simp
qed

lemma BfunE:
  assumes "Bfun f F"
  obtains B where "0 < B" and "eventually (λx. norm (f x) ≤ B) F"
  using assms unfolding Bfun_def by blast

lemma Cauchy_Bseq:
  assumes "Cauchy X" shows "Bseq X"
proof -
  have "∃y K. 0 < K ∧ (∃N. ∀n≥N. dist (X n) y ≤ K)"
    if "⋀m n. ⟦m ≥ M; n ≥ M⟧ ⟹ dist (X m) (X n) < 1" for M
    by (meson order.order_iff_strict that zero_less_one)
  with assms show ?thesis
    by (force simp: Cauchy_def Bfun_metric_def eventually_sequentially)
qed

subsubsection ‹Bounded Sequences›

lemma BseqI': "(⋀n. norm (X n) ≤ K) ⟹ Bseq X"
  by (intro BfunI) (auto simp: eventually_sequentially)

lemma Bseq_def: "Bseq X ⟷ (∃K>0. ∀n. norm (X n) ≤ K)"
  unfolding Bfun_def eventually_sequentially
proof safe
  fix N K
  assume "0 < K" "∀n≥N. norm (X n) ≤ K"
  then show "∃K>0. ∀n. norm (X n) ≤ K"
    by (intro exI[of _ "max (Max (norm ` X ` {..N})) K"] max.strict_coboundedI2)
       (auto intro!: imageI not_less[where 'a=nat, THEN iffD1] Max_ge simp: le_max_iff_disj)
qed auto

lemma BseqE: "Bseq X ⟹ (⋀K. 0 < K ⟹ ∀n. norm (X n) ≤ K ⟹ Q) ⟹ Q"
  unfolding Bseq_def by auto

lemma BseqD: "Bseq X ⟹ ∃K. 0 < K ∧ (∀n. norm (X n) ≤ K)"
  by (simp add: Bseq_def)

lemma BseqI: "0 < K ⟹ ∀n. norm (X n) ≤ K ⟹ Bseq X"
  by (auto simp: Bseq_def)

lemma Bseq_bdd_above: "Bseq X ⟹ bdd_above (range X)"
  for X :: "nat ⇒ real"
proof (elim BseqE, intro bdd_aboveI2)
  fix K n
  assume "0 < K" "∀n. norm (X n) ≤ K"
  then show "X n ≤ K"
    by (auto elim!: allE[of _ n])
qed

lemma Bseq_bdd_above': "Bseq X ⟹ bdd_above (range (λn. norm (X n)))"
  for X :: "nat ⇒ 'a :: real_normed_vector"
proof (elim BseqE, intro bdd_aboveI2)
  fix K n
  assume "0 < K" "∀n. norm (X n) ≤ K"
  then show "norm (X n) ≤ K"
    by (auto elim!: allE[of _ n])
qed

lemma Bseq_bdd_below: "Bseq X ⟹ bdd_below (range X)"
  for X :: "nat ⇒ real"
proof (elim BseqE, intro bdd_belowI2)
  fix K n
  assume "0 < K" "∀n. norm (X n) ≤ K"
  then show "- K ≤ X n"
    by (auto elim!: allE[of _ n])
qed

lemma Bseq_eventually_mono:
  assumes "eventually (λn. norm (f n) ≤ norm (g n)) sequentially" "Bseq g"
  shows "Bseq f"
proof -
  from assms(2) obtain K where "0 < K" and "eventually (λn. norm (g n) ≤ K) sequentially"
    unfolding Bfun_def by fast
  with assms(1) have "eventually (λn. norm (f n) ≤ K) sequentially"
    by (fast elim: eventually_elim2 order_trans)
  with ‹0 < K› show "Bseq f"
    unfolding Bfun_def by fast
qed

lemma lemma_NBseq_def: "(∃K > 0. ∀n. norm (X n) ≤ K) ⟷ (∃N. ∀n. norm (X n) ≤ real(Suc N))"
proof safe
  fix K :: real
  from reals_Archimedean2 obtain n :: nat where "K < real n" ..
  then have "K ≤ real (Suc n)" by auto
  moreover assume "∀m. norm (X m) ≤ K"
  ultimately have "∀m. norm (X m) ≤ real (Suc n)"
    by (blast intro: order_trans)
  then show "∃N. ∀n. norm (X n) ≤ real (Suc N)" ..
next
  show "⋀N. ∀n. norm (X n) ≤ real (Suc N) ⟹ ∃K>0. ∀n. norm (X n) ≤ K"
    using of_nat_0_less_iff by blast
qed

text ‹Alternative definition for ‹Bseq›.›
lemma Bseq_iff: "Bseq X ⟷ (∃N. ∀n. norm (X n) ≤ real(Suc N))"
  by (simp add: Bseq_def) (simp add: lemma_NBseq_def)

lemma lemma_NBseq_def2: "(∃K > 0. ∀n. norm (X n) ≤ K) = (∃N. ∀n. norm (X n) < real(Suc N))"
proof -
  have *: "⋀N. ∀n. norm (X n) ≤ 1 + real N ⟹
         ∃N. ∀n. norm (X n) < 1 + real N"
    by (metis add.commute le_less_trans less_add_one of_nat_Suc)
  then show ?thesis
    unfolding lemma_NBseq_def
    by (metis less_le_not_le not_less_iff_gr_or_eq of_nat_Suc)
qed

text ‹Yet another definition for Bseq.›
lemma Bseq_iff1a: "Bseq X ⟷ (∃N. ∀n. norm (X n) < real (Suc N))"
  by (simp add: Bseq_def lemma_NBseq_def2)

subsubsection ‹A Few More Equivalence Theorems for Boundedness›

text ‹Alternative formulation for boundedness.›
lemma Bseq_iff2: "Bseq X ⟷ (∃k > 0. ∃x. ∀n. norm (X n + - x) ≤ k)"
  by (metis BseqE BseqI' add.commute add_cancel_right_left add_uminus_conv_diff norm_add_leD
            norm_minus_cancel norm_minus_commute)

text ‹Alternative formulation for boundedness.›
lemma Bseq_iff3: "Bseq X ⟷ (∃k>0. ∃N. ∀n. norm (X n + - X N) ≤ k)"
  (is "?P ⟷ ?Q")
proof
  assume ?P
  then obtain K where *: "0 < K" and **: "⋀n. norm (X n) ≤ K"
    by (auto simp: Bseq_def)
  from * have "0 < K + norm (X 0)" by (rule order_less_le_trans) simp
  from ** have "∀n. norm (X n - X 0) ≤ K + norm (X 0)"
    by (auto intro: order_trans norm_triangle_ineq4)
  then have "∀n. norm (X n + - X 0) ≤ K + norm (X 0)"
    by simp
  with ‹0 < K + norm (X 0)› show ?Q by blast
next
  assume ?Q
  then show ?P by (auto simp: Bseq_iff2)
qed


subsubsection ‹Upper Bounds and Lubs of Bounded Sequences›

lemma Bseq_minus_iff: "Bseq (λn. - (X n) :: 'a::real_normed_vector) ⟷ Bseq X"
  by (simp add: Bseq_def)

lemma Bseq_add:
  fixes f :: "nat ⇒ 'a::real_normed_vector"
  assumes "Bseq f"
  shows "Bseq (λx. f x + c)"
proof -
  from assms obtain K where K: "⋀x. norm (f x) ≤ K"
    unfolding Bseq_def by blast
  {
    fix x :: nat
    have "norm (f x + c) ≤ norm (f x) + norm c" by (rule norm_triangle_ineq)
    also have "norm (f x) ≤ K" by (rule K)
    finally have "norm (f x + c) ≤ K + norm c" by simp
  }
  then show ?thesis by (rule BseqI')
qed

lemma Bseq_add_iff: "Bseq (λx. f x + c) ⟷ Bseq f"
  for f :: "nat ⇒ 'a::real_normed_vector"
  using Bseq_add[of f c] Bseq_add[of "λx. f x + c" "-c"] by auto

lemma Bseq_mult:
  fixes f g :: "nat ⇒ 'a::real_normed_field"
  assumes "Bseq f" and "Bseq g"
  shows "Bseq (λx. f x * g x)"
proof -
  from assms obtain K1 K2 where K: "norm (f x) ≤ K1" "K1 > 0" "norm (g x) ≤ K2" "K2 > 0"
    for x
    unfolding Bseq_def by blast
  then have "norm (f x * g x) ≤ K1 * K2" for x
    by (auto simp: norm_mult intro!: mult_mono)
  then show ?thesis by (rule BseqI')
qed

lemma Bfun_const [simp]: "Bfun (λ_. c) F"
  unfolding Bfun_metric_def by (auto intro!: exI[of _ c] exI[of _ "1::real"])

lemma Bseq_cmult_iff:
  fixes c :: "'a::real_normed_field"
  assumes "c ≠ 0"
  shows "Bseq (λx. c * f x) ⟷ Bseq f"
proof
  assume "Bseq (λx. c * f x)"
  with Bfun_const have "Bseq (λx. inverse c * (c * f x))"
    by (rule Bseq_mult)
  with ‹c ≠ 0› show "Bseq f"
    by (simp add: field_split_simps)
qed (intro Bseq_mult Bfun_const)

lemma Bseq_subseq: "Bseq f ⟹ Bseq (λx. f (g x))"
  for f :: "nat ⇒ 'a::real_normed_vector"
  unfolding Bseq_def by auto

lemma Bseq_Suc_iff: "Bseq (λn. f (Suc n)) ⟷ Bseq f"
  for f :: "nat ⇒ 'a::real_normed_vector"
  using Bseq_offset[of f 1] by (auto intro: Bseq_subseq)

lemma increasing_Bseq_subseq_iff:
  assumes "⋀x y. x ≤ y ⟹ norm (f x :: 'a::real_normed_vector) ≤ norm (f y)" "strict_mono g"
  shows "Bseq (λx. f (g x)) ⟷ Bseq f"
proof
  assume "Bseq (λx. f (g x))"
  then obtain K where K: "⋀x. norm (f (g x)) ≤ K"
    unfolding Bseq_def by auto
  {
    fix x :: nat
    from filterlim_subseq[OF assms(2)] obtain y where "g y ≥ x"
      by (auto simp: filterlim_at_top eventually_at_top_linorder)
    then have "norm (f x) ≤ norm (f (g y))"
      using assms(1) by blast
    also have "norm (f (g y)) ≤ K" by (rule K)
    finally have "norm (f x) ≤ K" .
  }
  then show "Bseq f" by (rule BseqI')
qed (use Bseq_subseq[of f g] in simp_all)

lemma nonneg_incseq_Bseq_subseq_iff:
  fixes f :: "nat ⇒ real"
    and g :: "nat ⇒ nat"
  assumes "⋀x. f x ≥ 0" "incseq f" "strict_mono g"
  shows "Bseq (λx. f (g x)) ⟷ Bseq f"
  using assms by (intro increasing_Bseq_subseq_iff) (auto simp: incseq_def)

lemma Bseq_eq_bounded: "range f ⊆ {a..b} ⟹ Bseq f"
  for a b :: real
proof (rule BseqI'[where K="max (norm a) (norm b)"])
  fix n assume "range f ⊆ {a..b}"
  then have "f n ∈ {a..b}"
    by blast
  then show "norm (f n) ≤ max (norm a) (norm b)"
    by auto
qed

lemma incseq_bounded: "incseq X ⟹ ∀i. X i ≤ B ⟹ Bseq X"
  for B :: real
  by (intro Bseq_eq_bounded[of X "X 0" B]) (auto simp: incseq_def)

lemma decseq_bounded: "decseq X ⟹ ∀i. B ≤ X i ⟹ Bseq X"
  for B :: real
  by (intro Bseq_eq_bounded[of X B "X 0"]) (auto simp: decseq_def)


subsubsection✐‹tag unimportant› ‹Polynomal function extremal theorem, from HOL Light›

lemma polyfun_extremal_lemma:
    fixes c :: "nat ⇒ 'a::real_normed_div_algebra"
  assumes "0 < e"
    shows "∃M. ∀z. M ≤ norm(z) ⟶ norm (∑i≤n. c(i) * z^i) ≤ e * norm(z) ^ (Suc n)"
proof (induct n)
  case 0 with assms
  show ?case
    apply (rule_tac x="norm (c 0) / e" in exI)
    apply (auto simp: field_simps)
    done
next
  case (Suc n)
  obtain M where M: "⋀z. M ≤ norm z ⟹ norm (∑i≤n. c i * z^i) ≤ e * norm z ^ Suc n"
    using Suc assms by blast
  show ?case
  proof (rule exI [where x= "max M (1 + norm(c(Suc n)) / e)"], clarsimp simp del: power_Suc)
    fix z::'a
    assume z1: "M ≤ norm z" and "1 + norm (c (Suc n)) / e ≤ norm z"
    then have z2: "e + norm (c (Suc n)) ≤ e * norm z"
      using assms by (simp add: field_simps)
    have "norm (∑i≤n. c i * z^i) ≤ e * norm z ^ Suc n"
      using M [OF z1] by simp
    then have "norm (∑i≤n. c i * z^i) + norm (c (Suc n) * z ^ Suc n) ≤ e * norm z ^ Suc n + norm (c (Suc n) * z ^ Suc n)"
      by simp
    then have "norm ((∑i≤n. c i * z^i) + c (Suc n) * z ^ Suc n) ≤ e * norm z ^ Suc n + norm (c (Suc n) * z ^ Suc n)"
      by (blast intro: norm_triangle_le elim: )
    also have "... ≤ (e + norm (c (Suc n))) * norm z ^ Suc n"
      by (simp add: norm_power norm_mult algebra_simps)
    also have "... ≤ (e * norm z) * norm z ^ Suc n"
      by (metis z2 mult.commute mult_left_mono norm_ge_zero norm_power)
    finally show "norm ((∑i≤n. c i * z^i) + c (Suc n) * z ^ Suc n) ≤ e * norm z ^ Suc (Suc n)"
      by simp
  qed
qed

lemma polyfun_extremal: (*COMPLEX_POLYFUN_EXTREMAL in HOL Light*)
    fixes c :: "nat ⇒ 'a::real_normed_div_algebra"
  assumes k: "c k ≠ 0" "1≤k" and kn: "k≤n"
    shows "eventually (λz. norm (∑i≤n. c(i) * z^i) ≥ B) at_infinity"
using kn
proof (induction n)
  case 0
  then show ?case
    using k by simp
next
  case (Suc m)
  show ?case
  proof (cases "c (Suc m) = 0")
    case True
    then show ?thesis using Suc k
      (*NOTE keep original non-terminal auto call for reproducibility*)
      by auto_orig (metis antisym_conv less_eq_Suc_le not_le)
  next
    case False
    then obtain M where M:
          "⋀z. M ≤ norm z ⟹ norm (∑i≤m. c i * z^i) ≤ norm (c (Suc m)) / 2 * norm z ^ Suc m"
      using polyfun_extremal_lemma [of "norm(c (Suc m)) / 2" c m] Suc
      by auto
    have "∃b. ∀z. b ≤ norm z ⟶ B ≤ norm (∑i≤Suc m. c i * z^i)"
    proof (rule exI [where x="max M (max 1 (¦B¦ / (norm(c (Suc m)) / 2)))"], clarsimp simp del: power_Suc)
      fix z::'a
      assume z1: "M ≤ norm z" "1 ≤ norm z"
         and "¦B¦ * 2 / norm (c (Suc m)) ≤ norm z"
      then have z2: "¦B¦ ≤ norm (c (Suc m)) * norm z / 2"
        using False by (simp add: field_simps)
      have nz: "norm z ≤ norm z ^ Suc m"
        by (metis ‹1 ≤ norm z› One_nat_def less_eq_Suc_le power_increasing power_one_right zero_less_Suc)
      have *: "⋀y x. norm (c (Suc m)) * norm z / 2 ≤ norm y - norm x ⟹ B ≤ norm (x + y)"
        by (metis abs_le_iff add.commute norm_diff_ineq order_trans z2)
      have "norm z * norm (c (Suc m)) + 2 * norm (∑i≤m. c i * z^i)
            ≤ norm (c (Suc m)) * norm z + norm (c (Suc m)) * norm z ^ Suc m"
        using M [of z] Suc z1  by auto
      also have "... ≤ 2 * (norm (c (Suc m)) * norm z ^ Suc m)"
        using nz by (simp add: mult_mono del: power_Suc)
      finally show "B ≤ norm ((∑i≤m. c i * z^i) + c (Suc m) * z ^ Suc m)"
        using Suc.IH
        apply (simp add: eventually_at_infinity)
        apply (rule *)
        apply (simp add: field_simps norm_mult norm_power)
        done
    qed
    then show ?thesis
      by (simp add: eventually_at_infinity)
  qed
qed

subsection ‹Convergence to Zero›

definition Zfun :: "('a ⇒ 'b::real_normed_vector) ⇒ 'a filter ⇒ bool"
  where "Zfun f F = (∀r>0. eventually (λx. norm (f x) < r) F)"

lemma ZfunI: "(⋀r. 0 < r ⟹ eventually (λx. norm (f x) < r) F) ⟹ Zfun f F"
  by (simp add: Zfun_def)

lemma ZfunD: "Zfun f F ⟹ 0 < r ⟹ eventually (λx. norm (f x) < r) F"
  by (simp add: Zfun_def)

lemma Zfun_ssubst: "eventually (λx. f x = g x) F ⟹ Zfun g F ⟹ Zfun f F"
  unfolding Zfun_def by (auto elim!: eventually_rev_mp)

lemma Zfun_zero: "Zfun (λx. 0) F"
  unfolding Zfun_def by simp

lemma Zfun_norm_iff: "Zfun (λx. norm (f x)) F = Zfun (λx. f x) F"
  unfolding Zfun_def by simp

lemma Zfun_imp_Zfun:
  assumes f: "Zfun f F"
    and g: "eventually (λx. norm (g x) ≤ norm (f x) * K) F"
  shows "Zfun (λx. g x) F"
proof (cases "0 < K")
  case K: True
  show ?thesis
  proof (rule ZfunI)
    fix r :: real
    assume "0 < r"
    then have "0 < r / K" using K by simp
    then have "eventually (λx. norm (f x) < r / K) F"
      using ZfunD [OF f] by blast
    with g show "eventually (λx. norm (g x) < r) F"
    proof eventually_elim
      case (elim x)
      then have "norm (f x) * K < r"
        by (simp add: pos_less_divide_eq K)
      then show ?case
        by (simp add: order_le_less_trans [OF elim(1)])
    qed
  qed
next
  case False
  then have K: "K ≤ 0" by (simp only: not_less)
  show ?thesis
  proof (rule ZfunI)
    fix r :: real
    assume "0 < r"
    from g show "eventually (λx. norm (g x) < r) F"
    proof eventually_elim
      case (elim x)
      also have "norm (f x) * K ≤ norm (f x) * 0"
        using K norm_ge_zero by (rule mult_left_mono)
      finally show ?case
        using ‹0 < r› by simp
    qed
  qed
qed

lemma Zfun_le: "Zfun g F ⟹ ∀x. norm (f x) ≤ norm (g x) ⟹ Zfun f F"
  by (erule Zfun_imp_Zfun [where K = 1]) simp

lemma Zfun_add:
  assumes f: "Zfun f F"
    and g: "Zfun g F"
  shows "Zfun (λx. f x + g x) F"
proof (rule ZfunI)
  fix r :: real
  assume "0 < r"
  then have r: "0 < r / 2" by simp
  have "eventually (λx. norm (f x) < r/2) F"
    using f r by (rule ZfunD)
  moreover
  have "eventually (λx. norm (g x) < r/2) F"
    using g r by (rule ZfunD)
  ultimately
  show "eventually (λx. norm (f x + g x) < r) F"
  proof eventually_elim
    case (elim x)
    have "norm (f x + g x) ≤ norm (f x) + norm (g x)"
      by (rule norm_triangle_ineq)
    also have "… < r/2 + r/2"
      using elim by (rule add_strict_mono)
    finally show ?case
      by simp
  qed
qed

lemma Zfun_minus: "Zfun f F ⟹ Zfun (λx. - f x) F"
  unfolding Zfun_def by simp

lemma Zfun_diff: "Zfun f F ⟹ Zfun g F ⟹ Zfun (λx. f x - g x) F"
  using Zfun_add [of f F "λx. - g x"] by (simp add: Zfun_minus)

lemma (in bounded_linear) Zfun:
  assumes g: "Zfun g F"
  shows "Zfun (λx. f (g x)) F"
proof -
  obtain K where "norm (f x) ≤ norm x * K" for x
    using bounded by blast
  then have "eventually (λx. norm (f (g x)) ≤ norm (g x) * K) F"
    by simp
  with g show ?thesis
    by (rule Zfun_imp_Zfun)
qed

lemma (in bounded_bilinear) Zfun:
  assumes f: "Zfun f F"
    and g: "Zfun g F"
  shows "Zfun (λx. f x ** g x) F"
proof (rule ZfunI)
  fix r :: real
  assume r: "0 < r"
  obtain K where K: "0 < K"
    and norm_le: "norm (x ** y) ≤ norm x * norm y * K" for x y
    using pos_bounded by blast
  from K have K': "0 < inverse K"
    by (rule positive_imp_inverse_positive)
  have "eventually (λx. norm (f x) < r) F"
    using f r by (rule ZfunD)
  moreover
  have "eventually (λx. norm (g x) < inverse K) F"
    using g K' by (rule ZfunD)
  ultimately
  show "eventually (λx. norm (f x ** g x) < r) F"
  proof eventually_elim
    case (elim x)
    have "norm (f x ** g x) ≤ norm (f x) * norm (g x) * K"
      by (rule norm_le)
    also have "norm (f x) * norm (g x) * K < r * inverse K * K"
      by (intro mult_strict_right_mono mult_strict_mono' norm_ge_zero elim K)
    also from K have "r * inverse K * K = r"
      by simp
    finally show ?case .
  qed
qed

lemma (in bounded_bilinear) Zfun_left: "Zfun f F ⟹ Zfun (λx. f x ** a) F"
  by (rule bounded_linear_left [THEN bounded_linear.Zfun])

lemma (in bounded_bilinear) Zfun_right: "Zfun f F ⟹ Zfun (λx. a ** f x) F"
  by (rule bounded_linear_right [THEN bounded_linear.Zfun])

lemmas Zfun_mult = bounded_bilinear.Zfun [OF bounded_bilinear_mult]
lemmas Zfun_mult_right = bounded_bilinear.Zfun_right [OF bounded_bilinear_mult]
lemmas Zfun_mult_left = bounded_bilinear.Zfun_left [OF bounded_bilinear_mult]

lemma tendsto_Zfun_iff: "(f ⤏ a) F = Zfun (λx. f x - a) F"
  by (simp only: tendsto_iff Zfun_def dist_norm)

lemma tendsto_0_le:
  "(f ⤏ 0) F ⟹ eventually (λx. norm (g x) ≤ norm (f x) * K) F ⟹ (g ⤏ 0) F"
  by (simp add: Zfun_imp_Zfun tendsto_Zfun_iff)


subsubsection ‹Distance and norms›

lemma tendsto_dist [tendsto_intros]:
  fixes l m :: "'a::metric_space"
  assumes f: "(f ⤏ l) F"
    and g: "(g ⤏ m) F"
  shows "((λx. dist (f x) (g x)) ⤏ dist l m) F"
proof (rule tendstoI)
  fix e :: real
  assume "0 < e"
  then have e2: "0 < e/2" by simp
  from tendstoD [OF f e2] tendstoD [OF g e2]
  show "eventually (λx. dist (dist (f x) (g x)) (dist l m) < e) F"
  proof (eventually_elim)
    case (elim x)
    then show "dist (dist (f x) (g x)) (dist l m) < e"
      unfolding dist_real_def
      using dist_triangle2 [of "f x" "g x" "l"]
        and dist_triangle2 [of "g x" "l" "m"]
        and dist_triangle3 [of "l" "m" "f x"]
        and dist_triangle [of "f x" "m" "g x"]
      by arith
  qed
qed

lemma continuous_dist[continuous_intros]:
  fixes f g :: "_ ⇒ 'a :: metric_space"
  shows "continuous F f ⟹ continuous F g ⟹ continuous F (λx. dist (f x) (g x))"
  unfolding continuous_def by (rule tendsto_dist)

lemma continuous_on_dist[continuous_intros]:
  fixes f g :: "_ ⇒ 'a :: metric_space"
  shows "continuous_on s f ⟹ continuous_on s g ⟹ continuous_on s (λx. dist (f x) (g x))"
  unfolding continuous_on_def by (auto intro: tendsto_dist)

lemma continuous_at_dist: "isCont (dist a) b"
  using continuous_on_dist [OF continuous_on_const continuous_on_id] continuous_on_eq_continuous_within by blast

lemma tendsto_norm [tendsto_intros]: "(f ⤏ a) F ⟹ ((λx. norm (f x)) ⤏ norm a) F"
  unfolding norm_conv_dist by (intro tendsto_intros)

lemma continuous_norm [continuous_intros]: "continuous F f ⟹ continuous F (λx. norm (f x))"
  unfolding continuous_def by (rule tendsto_norm)

lemma continuous_on_norm [continuous_intros]:
  "continuous_on s f ⟹ continuous_on s (λx. norm (f x))"
  unfolding continuous_on_def by (auto intro: tendsto_norm)

lemma continuous_on_norm_id [continuous_intros]: "continuous_on S norm"
  by (intro continuous_on_id continuous_on_norm)

lemma tendsto_norm_zero: "(f ⤏ 0) F ⟹ ((λx. norm (f x)) ⤏ 0) F"
  by (drule tendsto_norm) simp

lemma tendsto_norm_zero_cancel: "((λx. norm (f x)) ⤏ 0) F ⟹ (f ⤏ 0) F"
  unfolding tendsto_iff dist_norm by simp

lemma tendsto_norm_zero_iff: "((λx. norm (f x)) ⤏ 0) F ⟷ (f ⤏ 0) F"
  unfolding tendsto_iff dist_norm by simp

lemma tendsto_rabs [tendsto_intros]: "(f ⤏ l) F ⟹ ((λx. ¦f x¦) ⤏ ¦l¦) F"
  for l :: real
  by (fold real_norm_def) (rule tendsto_norm)

lemma continuous_rabs [continuous_intros]:
  "continuous F f ⟹ continuous F (λx. ¦f x :: real¦)"
  unfolding real_norm_def[symmetric] by (rule continuous_norm)

lemma continuous_on_rabs [continuous_intros]:
  "continuous_on s f ⟹ continuous_on s (λx. ¦f x :: real¦)"
  unfolding real_norm_def[symmetric] by (rule continuous_on_norm)

lemma tendsto_rabs_zero: "(f ⤏ (0::real)) F ⟹ ((λx. ¦f x¦) ⤏ 0) F"
  by (fold real_norm_def) (rule tendsto_norm_zero)

lemma tendsto_rabs_zero_cancel: "((λx. ¦f x¦) ⤏ (0::real)) F ⟹ (f ⤏ 0) F"
  by (fold real_norm_def) (rule tendsto_norm_zero_cancel)

lemma tendsto_rabs_zero_iff: "((λx. ¦f x¦) ⤏ (0::real)) F ⟷ (f ⤏ 0) F"
  by (fold real_norm_def) (rule tendsto_norm_zero_iff)


subsection ‹Topological Monoid›

class topological_monoid_add = topological_space + monoid_add +
  assumes tendsto_add_Pair: "LIM x (nhds a ×⇩F nhds b). fst x + snd x :> nhds (a + b)"

class topological_comm_monoid_add = topological_monoid_add + comm_monoid_add

lemma tendsto_add [tendsto_intros]:
  fixes a b :: "'a::topological_monoid_add"
  shows "(f ⤏ a) F ⟹ (g ⤏ b) F ⟹ ((λx. f x + g x) ⤏ a + b) F"
  using filterlim_compose[OF tendsto_add_Pair, of "λx. (f x, g x)" a b F]
  by (simp add: nhds_prod[symmetric] tendsto_Pair)

lemma continuous_add [continuous_intros]:
  fixes f g :: "_ ⇒ 'b::topological_monoid_add"
  shows "continuous F f ⟹ continuous F g ⟹ continuous F (λx. f x + g x)"
  unfolding continuous_def by (rule tendsto_add)

lemma continuous_on_add [continuous_intros]:
  fixes f g :: "_ ⇒ 'b::topological_monoid_add"
  shows "continuous_on s f ⟹ continuous_on s g ⟹ continuous_on s (λx. f x + g x)"
  unfolding continuous_on_def by (auto intro: tendsto_add)

lemma tendsto_add_zero:
  fixes f g :: "_ ⇒ 'b::topological_monoid_add"
  shows "(f ⤏ 0) F ⟹ (g ⤏ 0) F ⟹ ((λx. f x + g x) ⤏ 0) F"
  by (drule (1) tendsto_add) simp

lemma tendsto_sum [tendsto_intros]:
  fixes f :: "'a ⇒ 'b ⇒ 'c::topological_comm_monoid_add"
  shows "(⋀i. i ∈ I ⟹ (f i ⤏ a i) F) ⟹ ((λx. ∑i∈I. f i x) ⤏ (∑i∈I. a i)) F"
  by (induct I rule: infinite_finite_induct) (simp_all add: tendsto_add)

lemma tendsto_null_sum:
  fixes f :: "'a ⇒ 'b ⇒ 'c::topological_comm_monoid_add"
  assumes "⋀i. i ∈ I ⟹ ((λx. f x i) ⤏ 0) F"
  shows "((λi. sum (f i) I) ⤏ 0) F"
  using tendsto_sum [of I "λx y. f y x" "λx. 0"] assms by simp

lemma continuous_sum [continuous_intros]:
  fixes f :: "'a ⇒ 'b::t2_space ⇒ 'c::topological_comm_monoid_add"
  shows "(⋀i. i ∈ I ⟹ continuous F (f i)) ⟹ continuous F (λx. ∑i∈I. f i x)"
  unfolding continuous_def by (rule tendsto_sum)

lemma continuous_on_sum [continuous_intros]:
  fixes f :: "'a ⇒ 'b::topological_space ⇒ 'c::topological_comm_monoid_add"
  shows "(⋀i. i ∈ I ⟹ continuous_on S (f i)) ⟹ continuous_on S (λx. ∑i∈I. f i x)"
  unfolding continuous_on_def by (auto intro: tendsto_sum)

instance nat :: topological_comm_monoid_add
  by standard
    (simp add: nhds_discrete principal_prod_principal filterlim_principal eventually_principal)

instance int :: topological_comm_monoid_add
  by standard
    (simp add: nhds_discrete principal_prod_principal filterlim_principal eventually_principal)


subsubsection ‹Topological group›

class topological_group_add = topological_monoid_add + group_add +
  assumes tendsto_uminus_nhds: "(uminus ⤏ - a) (nhds a)"
begin

lemma tendsto_minus [tendsto_intros]: "(f ⤏ a) F ⟹ ((λx. - f x) ⤏ - a) F"
  by (rule filterlim_compose[OF tendsto_uminus_nhds])

end

class topological_ab_group_add = topological_group_add + ab_group_add

instance topological_ab_group_add < topological_comm_monoid_add ..

lemma continuous_minus [continuous_intros]: "continuous F f ⟹ continuous F (λx. - f x)"
  for f :: "'a::t2_space ⇒ 'b::topological_group_add"
  unfolding continuous_def by (rule tendsto_minus)

lemma continuous_on_minus [continuous_intros]: "continuous_on s f ⟹ continuous_on s (λx. - f x)"
  for f :: "_ ⇒ 'b::topological_group_add"
  unfolding continuous_on_def by (auto intro: tendsto_minus)

lemma tendsto_minus_cancel: "((λx. - f x) ⤏ - a) F ⟹ (f ⤏ a) F"
  for a :: "'a::topological_group_add"
  by (drule tendsto_minus) simp

lemma tendsto_minus_cancel_left:
  "(f ⤏ - (y::_::topological_group_add)) F ⟷ ((λx. - f x) ⤏ y) F"
  using tendsto_minus_cancel[of f "- y" F]  tendsto_minus[of f "- y" F]
  by auto

lemma tendsto_diff [tendsto_intros]:
  fixes a b :: "'a::topological_group_add"
  shows "(f ⤏ a) F ⟹ (g ⤏ b) F ⟹ ((λx. f x - g x) ⤏ a - b) F"
  using tendsto_add [of f a F "λx. - g x" "- b"] by (simp add: tendsto_minus)

lemma continuous_diff [continuous_intros]:
  fixes f g :: "'a::t2_space ⇒ 'b::topological_group_add"
  shows "continuous F f ⟹ continuous F g ⟹ continuous F (λx. f x - g x)"
  unfolding continuous_def by (rule tendsto_diff)

lemma continuous_on_diff [continuous_intros]:
  fixes f g :: "_ ⇒ 'b::topological_group_add"
  shows "continuous_on s f ⟹ continuous_on s g ⟹ continuous_on s (λx. f x - g x)"
  unfolding continuous_on_def by (auto intro: tendsto_diff)

lemma continuous_on_op_minus: "continuous_on (s::'a::topological_group_add set) ((-) x)"
  by (rule continuous_intros | simp)+

instance real_normed_vector < topological_ab_group_add
proof
  fix a b :: 'a
  show "((λx. fst x + snd x) ⤏ a + b) (nhds a ×⇩F nhds b)"
    unfolding tendsto_Zfun_iff add_diff_add
    using tendsto_fst[OF filterlim_ident, of "(a,b)"] tendsto_snd[OF filterlim_ident, of "(a,b)"]
    by (intro Zfun_add)
       (auto simp: tendsto_Zfun_iff[symmetric] nhds_prod[symmetric] intro!: tendsto_fst)
  show "(uminus ⤏ - a) (nhds a)"
    unfolding tendsto_Zfun_iff minus_diff_minus
    using filterlim_ident[of "nhds a"]
    by (intro Zfun_minus) (simp add: tendsto_Zfun_iff)
qed

lemmas real_tendsto_sandwich = tendsto_sandwich[where 'a=real]


subsubsection ‹Linear operators and multiplication›

lemma linear_times [simp]: "linear (λx. c * x)"
  for c :: "'a::real_algebra"
  by (auto simp: linearI distrib_left)

lemma (in bounded_linear) tendsto: "(g ⤏ a) F ⟹ ((λx. f (g x)) ⤏ f a) F"
  by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun)

lemma (in bounded_linear) continuous: "continuous F g ⟹ continuous F (λx. f (g x))"
  using tendsto[of g _ F] by (auto simp: continuous_def)

lemma (in bounded_linear) continuous_on: "continuous_on s g ⟹ continuous_on s (λx. f (g x))"
  using tendsto[of g] by (auto simp: continuous_on_def)

lemma (in bounded_linear) tendsto_zero: "(g ⤏ 0) F ⟹ ((λx. f (g x)) ⤏ 0) F"
  by (drule tendsto) (simp only: zero)

lemma (in bounded_bilinear) tendsto:
  "(f ⤏ a) F ⟹ (g ⤏ b) F ⟹ ((λx. f x ** g x) ⤏ a ** b) F"
  by (simp only: tendsto_Zfun_iff prod_diff_prod Zfun_add Zfun Zfun_left Zfun_right)

lemma (in bounded_bilinear) continuous:
  "continuous F f ⟹ continuous F g ⟹ continuous F (λx. f x ** g x)"
  using tendsto[of f _ F g] by (auto simp: continuous_def)

lemma (in bounded_bilinear) continuous_on:
  "continuous_on s f ⟹ continuous_on s g ⟹ continuous_on s (λx. f x ** g x)"
  using tendsto[of f _ _ g] by (auto simp: continuous_on_def)

lemma (in bounded_bilinear) tendsto_zero:
  assumes f: "(f ⤏ 0) F"
    and g: "(g ⤏ 0) F"
  shows "((λx. f x ** g x) ⤏ 0) F"
  using tendsto [OF f g] by (simp add: zero_left)

lemma (in bounded_bilinear) tendsto_left_zero:
  "(f ⤏ 0) F ⟹ ((λx. f x ** c) ⤏ 0) F"
  by (rule bounded_linear.tendsto_zero [OF bounded_linear_left])

lemma (in bounded_bilinear) tendsto_right_zero:
  "(f ⤏ 0) F ⟹ ((λx. c ** f x) ⤏ 0) F"
  by (rule bounded_linear.tendsto_zero [OF bounded_linear_right])

lemmas tendsto_of_real [tendsto_intros] =
  bounded_linear.tendsto [OF bounded_linear_of_real]

lemmas tendsto_scaleR [tendsto_intros] =
  bounded_bilinear.tendsto [OF bounded_bilinear_scaleR]


text‹Analogous type class for multiplication›
class topological_semigroup_mult = topological_space + semigroup_mult +
  assumes tendsto_mult_Pair: "LIM x (nhds a ×⇩F nhds b). fst x * snd x :> nhds (a * b)"

instance real_normed_algebra < topological_semigroup_mult
proof
  fix a b :: 'a
  show "((λx. fst x * snd x) ⤏ a * b) (nhds a ×⇩F nhds b)"
    unfolding nhds_prod[symmetric]
    using tendsto_fst[OF filterlim_ident, of "(a,b)"] tendsto_snd[OF filterlim_ident, of "(a,b)"]
    by (simp add: bounded_bilinear.tendsto [OF bounded_bilinear_mult])
qed

lemma tendsto_mult [tendsto_intros]:
  fixes a b :: "'a::topological_semigroup_mult"
  shows "(f ⤏ a) F ⟹ (g ⤏ b) F ⟹ ((λx. f x * g x) ⤏ a * b) F"
  using filterlim_compose[OF tendsto_mult_Pair, of "λx. (f x, g x)" a b F]
  by (simp add: nhds_prod[symmetric] tendsto_Pair)

lemma tendsto_mult_left: "(f ⤏ l) F ⟹ ((λx. c * (f x)) ⤏ c * l) F"
  for c :: "'a::topological_semigroup_mult"
  by (rule tendsto_mult [OF tendsto_const])

lemma tendsto_mult_right: "(f ⤏ l) F ⟹ ((λx. (f x) * c) ⤏ l * c) F"
  for c :: "'a::topological_semigroup_mult"
  by (rule tendsto_mult [OF _ tendsto_const])

lemma tendsto_mult_left_iff [simp]:
   "c ≠ 0 ⟹ tendsto(λx. c * f x) (c * l) F ⟷ tendsto f l F" for c :: "'a::{topological_semigroup_mult,field}"
  by (auto simp: tendsto_mult_left dest: tendsto_mult_left [where c = "1/c"])

lemma tendsto_mult_right_iff [simp]:
   "c ≠ 0 ⟹ tendsto(λx. f x * c) (l * c) F ⟷ tendsto f l F" for c :: "'a::{topological_semigroup_mult,field}"
  by (auto simp: tendsto_mult_right dest: tendsto_mult_left [where c = "1/c"])

lemma tendsto_zero_mult_left_iff [simp]:
  fixes c::"'a::{topological_semigroup_mult,field}" assumes "c ≠ 0" shows "(λn. c * a n)⇢ 0 ⟷ a ⇢ 0"
  (*NEW*)
  (*NOTE the two passed rules contain meta variables. If we insert them to the goal state with
  "using", any meta variable instantiation of the rule will be persistent to the follow-up search
  (root cause: Isabelle uses prenex polymorphism and thus there is no universal type abstraction to
  the rule when inserted to the goal state).
  In particular, an unwanted instantiation will block follow-up usages of the rule. Passing the
  rules explicitly to the classical reasoner will make them available with with several possible
  instantiations*)
  using assms by (fastforce dest: tendsto_mult_left tendsto_mult_left_iff)
  (*ORIG*)
  (* using assms tendsto_mult_left tendsto_mult_left_iff by fastforce *)

lemma tendsto_zero_mult_right_iff [simp]:
  fixes c::"'a::{topological_semigroup_mult,field}" assumes "c ≠ 0" shows "(λn. a n * c)⇢ 0 ⟷ a ⇢ 0"
  (*NEW*)
  using assms by (fastforce dest: tendsto_mult_right tendsto_mult_right_iff)
  (*ORIG*)
  (* using assms tendsto_mult_right tendsto_mult_right_iff by fastforce *)

lemma tendsto_zero_divide_iff [simp]:
  fixes c::"'a::{topological_semigroup_mult,field}" assumes "c ≠ 0" shows "(λn. a n / c)⇢ 0 ⟷ a ⇢ 0"
  using tendsto_zero_mult_right_iff [of "1/c" a] assms by (simp add: field_simps)

lemma lim_const_over_n [tendsto_intros]:
  fixes a :: "'a::real_normed_field"
  shows "(λn. a / of_nat n) ⇢ 0"
  using tendsto_mult [OF tendsto_const [of a] lim_1_over_n] by simp

lemmas continuous_of_real [continuous_intros] =
  bounded_linear.continuous [OF bounded_linear_of_real]

lemmas continuous_scaleR [continuous_intros] =
  bounded_bilinear.continuous [OF bounded_bilinear_scaleR]

lemmas continuous_mult [continuous_intros] =
  bounded_bilinear.continuous [OF bounded_bilinear_mult]

lemmas continuous_on_of_real [continuous_intros] =
  bounded_linear.continuous_on [OF bounded_linear_of_real]

lemmas continuous_on_scaleR [continuous_intros] =
  bounded_bilinear.continuous_on [OF bounded_bilinear_scaleR]

lemmas continuous_on_mult [continuous_intros] =
  bounded_bilinear.continuous_on [OF bounded_bilinear_mult]

lemmas tendsto_mult_zero =
  bounded_bilinear.tendsto_zero [OF bounded_bilinear_mult]

lemmas tendsto_mult_left_zero =
  bounded_bilinear.tendsto_left_zero [OF bounded_bilinear_mult]

lemmas tendsto_mult_right_zero =
  bounded_bilinear.tendsto_right_zero [OF bounded_bilinear_mult]


lemma continuous_mult_left:
  fixes c::"'a::real_normed_algebra"
  shows "continuous F f ⟹ continuous F (λx. c * f x)"
by (rule continuous_mult [OF continuous_const])

lemma continuous_mult_right:
  fixes c::"'a::real_normed_algebra"
  shows "continuous F f ⟹ continuous F (λx. f x * c)"
by (rule continuous_mult [OF _ continuous_const])

lemma continuous_on_mult_left:
  fixes c::"'a::real_normed_algebra"
  shows "continuous_on s f ⟹ continuous_on s (λx. c * f x)"
by (rule continuous_on_mult [OF continuous_on_const])

lemma continuous_on_mult_right:
  fixes c::"'a::real_normed_algebra"
  shows "continuous_on s f ⟹ continuous_on s (λx. f x * c)"
by (rule continuous_on_mult [OF _ continuous_on_const])

lemma continuous_on_mult_const [simp]:
  fixes c::"'a::real_normed_algebra"
  shows "continuous_on s ((*) c)"
  by (intro continuous_on_mult_left continuous_on_id)

lemma tendsto_divide_zero:
  fixes c :: "'a::real_normed_field"
  shows "(f ⤏ 0) F ⟹ ((λx. f x / c) ⤏ 0) F"
  by (cases "c=0") (simp_all add: divide_inverse tendsto_mult_left_zero)

lemma tendsto_power [tendsto_intros]: "(f ⤏ a) F ⟹ ((λx. f x ^ n) ⤏ a ^ n) F"
  for f :: "'a ⇒ 'b::{power,real_normed_algebra}"
  by (induct n) (simp_all add: tendsto_mult)

lemma tendsto_null_power: "⟦(f ⤏ 0) F; 0 < n⟧ ⟹ ((λx. f x ^ n) ⤏ 0) F"
    for f :: "'a ⇒ 'b::{power,real_normed_algebra_1}"
  using tendsto_power [of f 0 F n] by (simp add: power_0_left)

lemma continuous_power [continuous_intros]: "continuous F f ⟹ continuous F (λx. (f x)^n)"
  for f :: "'a::t2_space ⇒ 'b::{power,real_normed_algebra}"
  unfolding continuous_def by (rule tendsto_power)

lemma continuous_on_power [continuous_intros]:
  fixes f :: "_ ⇒ 'b::{power,real_normed_algebra}"
  shows "continuous_on s f ⟹ continuous_on s (λx. (f x)^n)"
  unfolding continuous_on_def by (auto intro: tendsto_power)

lemma tendsto_prod [tendsto_intros]:
  fixes f :: "'a ⇒ 'b ⇒ 'c::{real_normed_algebra,comm_ring_1}"
  shows "(⋀i. i ∈ S ⟹ (f i ⤏ L i) F) ⟹ ((λx. ∏i∈S. f i x) ⤏ (∏i∈S. L i)) F"
  by (induct S rule: infinite_finite_induct) (simp_all add: tendsto_mult)

lemma continuous_prod [continuous_intros]:
  fixes f :: "'a ⇒ 'b::t2_space ⇒ 'c::{real_normed_algebra,comm_ring_1}"
  shows "(⋀i. i ∈ S ⟹ continuous F (f i)) ⟹ continuous F (λx. ∏i∈S. f i x)"
  unfolding continuous_def by (rule tendsto_prod)

lemma continuous_on_prod [continuous_intros]:
  fixes f :: "'a ⇒ _ ⇒ 'c::{real_normed_algebra,comm_ring_1}"
  shows "(⋀i. i ∈ S ⟹ continuous_on s (f i)) ⟹ continuous_on s (λx. ∏i∈S. f i x)"
  unfolding continuous_on_def by (auto intro: tendsto_prod)

lemma tendsto_of_real_iff:
  "((λx. of_real (f x) :: 'a::real_normed_div_algebra) ⤏ of_real c) F ⟷ (f ⤏ c) F"
  unfolding tendsto_iff by simp

lemma tendsto_add_const_iff:
  "((λx. c + f x :: 'a::topological_group_add) ⤏ c + d) F ⟷ (f ⤏ d) F"
  using tendsto_add[OF tendsto_const[of c], of f d]
    and tendsto_add[OF tendsto_const[of "-c"], of "λx. c + f x" "c + d"] by auto


class topological_monoid_mult = topological_semigroup_mult + monoid_mult
class topological_comm_monoid_mult = topological_monoid_mult + comm_monoid_mult

lemma tendsto_power_strong [tendsto_intros]:
  fixes f :: "_ ⇒ 'b :: topological_monoid_mult"
  assumes "(f ⤏ a) F" "(g ⤏ b) F"
  shows   "((λx. f x ^ g x) ⤏ a ^ b) F"
proof -
  have "((λx. f x ^ b) ⤏ a ^ b) F"
    by (induction b) (auto intro: tendsto_intros assms)
  also from assms(2) have "eventually (λx. g x = b) F"
    by (simp add: nhds_discrete filterlim_principal)
  hence "eventually (λx. f x ^ b = f x ^ g x) F"
    by eventually_elim simp
  hence "((λx. f x ^ b) ⤏ a ^ b) F ⟷ ((λx. f x ^ g x) ⤏ a ^ b) F"
    by (intro filterlim_cong refl)
  finally show ?thesis .
qed

lemma continuous_mult' [continuous_intros]:
  fixes f g :: "_ ⇒ 'b::topological_semigroup_mult"
  shows "continuous F f ⟹ continuous F g ⟹ continuous F (λx. f x * g x)"
  unfolding continuous_def by (rule tendsto_mult)

lemma continuous_power' [continuous_intros]:
  fixes f :: "_ ⇒ 'b::topological_monoid_mult"
  shows "continuous F f ⟹ continuous F g ⟹ continuous F (λx. f x ^ g x)"
  unfolding continuous_def by (rule tendsto_power_strong) auto

lemma continuous_on_mult' [continuous_intros]:
  fixes f g :: "_ ⇒ 'b::topological_semigroup_mult"
  shows "continuous_on A f ⟹ continuous_on A g ⟹ continuous_on A (λx. f x * g x)"
  unfolding continuous_on_def by (auto intro: tendsto_mult)

lemma continuous_on_power' [continuous_intros]:
  fixes f :: "_ ⇒ 'b::topological_monoid_mult"
  shows "continuous_on A f ⟹ continuous_on A g ⟹ continuous_on A (λx. f x ^ g x)"
  unfolding continuous_on_def by (auto intro: tendsto_power_strong)

lemma tendsto_mult_one:
  fixes f g :: "_ ⇒ 'b::topological_monoid_mult"
  shows "(f ⤏ 1) F ⟹ (g ⤏ 1) F ⟹ ((λx. f x * g x) ⤏ 1) F"
  by (drule (1) tendsto_mult) simp

lemma tendsto_prod' [tendsto_intros]:
  fixes f :: "'a ⇒ 'b ⇒ 'c::topological_comm_monoid_mult"
  shows "(⋀i. i ∈ I ⟹ (f i ⤏ a i) F) ⟹ ((λx. ∏i∈I. f i x) ⤏ (∏i∈I. a i)) F"
  by (induct I rule: infinite_finite_induct) (simp_all add: tendsto_mult)

lemma tendsto_one_prod':
  fixes f :: "'a ⇒ 'b ⇒ 'c::topological_comm_monoid_mult"
  assumes "⋀i. i ∈ I ⟹ ((λx. f x i) ⤏ 1) F"
  shows "((λi. prod (f i) I) ⤏ 1) F"
  using tendsto_prod' [of I "λx y. f y x" "λx. 1"] assms by simp

lemma LIMSEQ_prod_0:
  fixes f :: "nat ⇒ 'a::{semidom,topological_space}"
  assumes "f i = 0"
  shows "(λn. prod f {..n}) ⇢ 0"
proof (subst tendsto_cong)
  show "∀⇩F n in sequentially. prod f {..n} = 0"
    using assms eventually_at_top_linorder
    (*NEW*)
    by (auto run exec: Zip.Depth_First.all')
    (*ORIG*)
    (* by (auto) *)
qed auto

lemma LIMSEQ_prod_nonneg:
  fixes f :: "nat ⇒ 'a::{linordered_semidom,linorder_topology}"
  assumes 0: "⋀n. 0 ≤ f n" and a: "(λn. prod f {..n}) ⇢ a"
  shows "a ≥ 0"
  by (simp add: "0" prod_nonneg LIMSEQ_le_const [OF a])

lemma continuous_prod' [continuous_intros]:
  fixes f :: "'a ⇒ 'b::t2_space ⇒ 'c::topological_comm_monoid_mult"
  shows "(⋀i. i ∈ I ⟹ continuous F (f i)) ⟹ continuous F (λx. ∏i∈I. f i x)"
  unfolding continuous_def by (rule tendsto_prod')

lemma continuous_on_prod' [continuous_intros]:
  fixes f :: "'a ⇒ 'b::topological_space ⇒ 'c::topological_comm_monoid_mult"
  shows "(⋀i. i ∈ I ⟹ continuous_on S (f i)) ⟹ continuous_on S (λx. ∏i∈I. f i x)"
  unfolding continuous_on_def by (auto intro: tendsto_prod')

instance nat :: topological_comm_monoid_mult
  by standard
    (simp add: nhds_discrete principal_prod_principal filterlim_principal eventually_principal)

instance int :: topological_comm_monoid_mult
  by standard
    (simp add: nhds_discrete principal_prod_principal filterlim_principal eventually_principal)

class comm_real_normed_algebra_1 = real_normed_algebra_1 + comm_monoid_mult

context real_normed_field
begin

subclass comm_real_normed_algebra_1
proof
  from norm_mult[of "1 :: 'a" 1] show "norm 1 = 1" by simp
qed (simp_all add: norm_mult)

end

subsubsection ‹Inverse and division›

lemma (in bounded_bilinear) Zfun_prod_Bfun:
  assumes f: "Zfun f F"
    and g: "Bfun g F"
  shows "Zfun (λx. f x ** g x) F"
proof -
  obtain K where K: "0 ≤ K"
    and norm_le: "⋀x y. norm (x ** y) ≤ norm x * norm y * K"
    using nonneg_bounded by blast
  obtain B where B: "0 < B"
    and norm_g: "eventually (λx. norm (g x) ≤ B) F"
    using g by (rule BfunE)
  have "eventually (λx. norm (f x ** g x) ≤ norm (f x) * (B * K)) F"
  using norm_g proof eventually_elim
    case (elim x)
    have "norm (f x ** g x) ≤ norm (f x) * norm (g x) * K"
      by (rule norm_le)
    also have "… ≤ norm (f x) * B * K"
      by (intro mult_mono' order_refl norm_g norm_ge_zero mult_nonneg_nonneg K elim)
    also have "… = norm (f x) * (B * K)"
      by (rule mult.assoc)
    finally show "norm (f x ** g x) ≤ norm (f x) * (B * K)" .
  qed
  with f show ?thesis
    by (rule Zfun_imp_Zfun)
qed

lemma (in bounded_bilinear) Bfun_prod_Zfun:
  assumes f: "Bfun f F"
    and g: "Zfun g F"
  shows "Zfun (λx. f x ** g x) F"
  using flip g f by (rule bounded_bilinear.Zfun_prod_Bfun)

lemma Bfun_inverse:
  fixes a :: "'a::real_normed_div_algebra"
  assumes f: "(f ⤏ a) F"
  assumes a: "a ≠ 0"
  shows "Bfun (λx. inverse (f x)) F"
proof -
  from a have "0 < norm a" by simp
  then have "∃r>0. r < norm a" by (rule dense)
  then obtain r where r1: "0 < r" and r2: "r < norm a"
    by blast
  have "eventually (λx. dist (f x) a < r) F"
    using tendstoD [OF f r1] by blast
  then have "eventually (λx. norm (inverse (f x)) ≤ inverse (norm a - r)) F"
  proof eventually_elim
    case (elim x)
    then have 1: "norm (f x - a) < r"
      by (simp add: dist_norm)
    then have 2: "f x ≠ 0" using r2 by auto
    then have "norm (inverse (f x)) = inverse (norm (f x))"
      by (rule nonzero_norm_inverse)
    also have "… ≤ inverse (norm a - r)"
    proof (rule le_imp_inverse_le)
      show "0 < norm a - r"
        using r2 by simp
      have "norm a - norm (f x) ≤ norm (a - f x)"
        by (rule norm_triangle_ineq2)
      also have "… = norm (f x - a)"
        by (rule norm_minus_commute)
      also have "… < r" using 1 .
      finally show "norm a - r ≤ norm (f x)"
        by simp
    qed
    finally show "norm (inverse (f x)) ≤ inverse (norm a - r)" .
  qed
  then show ?thesis by (rule BfunI)
qed

lemma tendsto_inverse [tendsto_intros]:
  fixes a :: "'a::real_normed_div_algebra"
  assumes f: "(f ⤏ a) F"
    and a: "a ≠ 0"
  shows "((λx. inverse (f x)) ⤏ inverse a) F"
proof -
  from a have "0 < norm a" by simp
  with f have "eventually (λx. dist (f x) a < norm a) F"
    by (rule tendstoD)
  then have "eventually (λx. f x ≠ 0) F"
    unfolding dist_norm by (auto elim!: eventually_mono)
  with a have "eventually (λx. inverse (f x) - inverse a =
    - (inverse (f x) * (f x - a) * inverse a)) F"
    by (auto elim!: eventually_mono simp: inverse_diff_inverse)
  moreover have "Zfun (λx. - (inverse (f x) * (f x - a) * inverse a)) F"
    by (intro Zfun_minus Zfun_mult_left
      bounded_bilinear.Bfun_prod_Zfun [OF bounded_bilinear_mult]
      Bfun_inverse [OF f a] f [unfolded tendsto_Zfun_iff])
  ultimately show ?thesis
    unfolding tendsto_Zfun_iff by (rule Zfun_ssubst)
qed

lemma continuous_inverse:
  fixes f :: "'a::t2_space ⇒ 'b::real_normed_div_algebra"
  assumes "continuous F f"
    and "f (Lim F (λx. x)) ≠ 0"
  shows "continuous F (λx. inverse (f x))"
  using assms unfolding continuous_def by (rule tendsto_inverse)

lemma continuous_at_within_inverse[continuous_intros]:
  fixes f :: "'a::t2_space ⇒ 'b::real_normed_div_algebra"
  assumes "continuous (at a within s) f"
    and "f a ≠ 0"
  shows "continuous (at a within s) (λx. inverse (f x))"
  using assms unfolding continuous_within by (rule tendsto_inverse)

lemma continuous_on_inverse[continuous_intros]:
  fixes f :: "'a::topological_space ⇒ 'b::real_normed_div_algebra"
  assumes "continuous_on s f"
    and "∀x∈s. f x ≠ 0"
  shows "continuous_on s (λx. inverse (f x))"
  using assms unfolding continuous_on_def by (blast intro: tendsto_inverse)

lemma tendsto_divide [tendsto_intros]:
  fixes a b :: "'a::real_normed_field"
  shows "(f ⤏ a) F ⟹ (g ⤏ b) F ⟹ b ≠ 0 ⟹ ((λx. f x / g x) ⤏ a / b) F"
  by (simp add: tendsto_mult tendsto_inverse divide_inverse)

lemma continuous_divide:
  fixes f g :: "'a::t2_space ⇒ 'b::real_normed_field"
  assumes "continuous F f"
    and "continuous F g"
    and "g (Lim F (λx. x)) ≠ 0"
  shows "continuous F (λx. (f x) / (g x))"
  using assms unfolding continuous_def by (rule tendsto_divide)

lemma continuous_at_within_divide[continuous_intros]:
  fixes f g :: "'a::t2_space ⇒ 'b::real_normed_field"
  assumes "continuous (at a within s) f" "continuous (at a within s) g"
    and "g a ≠ 0"
  shows "continuous (at a within s) (λx. (f x) / (g x))"
  using assms unfolding continuous_within by (rule tendsto_divide)

lemma isCont_divide[continuous_intros, simp]:
  fixes f g :: "'a::t2_space ⇒ 'b::real_normed_field"
  assumes "isCont f a" "isCont g a" "g a ≠ 0"
  shows "isCont (λx. (f x) / g x) a"
  using assms unfolding continuous_at by (rule tendsto_divide)

lemma continuous_on_divide[continuous_intros]:
  fixes f :: "'a::topological_space ⇒ 'b::real_normed_field"
  assumes "continuous_on s f" "continuous_on s g"
    and "∀x∈s. g x ≠ 0"
  shows "continuous_on s (λx. (f x) / (g x))"
  using assms unfolding continuous_on_def by (blast intro: tendsto_divide)

lemma continuous_cmult_left_iff:
  fixes c::"'a::real_normed_field"
  assumes "c ≠ 0"
  shows "continuous F (λx. c * f x) ⟷ continuous F f"
  by (simp add: assms continuous_def)

lemma continuous_cmult_right_iff:
  fixes c::"'a::real_normed_field"
  assumes "c ≠ 0"
  shows "continuous F (λx. f x * c) ⟷ continuous F f"
  by (simp add: assms continuous_def)

lemma continuous_cdivide_iff:
  fixes c::"'a::real_normed_field"
  assumes "c ≠ 0"
  shows "continuous F (λx. f x / c) ⟷ continuous F f"
  using assms by (auto simp: continuous_def divide_inverse)

lemma continuous_cong:
  assumes "eventually (λx. f x = g x) F" "f (Lim F (λx. x)) = g (Lim F (λx. x))"
  shows "continuous F f ⟷ continuous F g"
  unfolding continuous_def using assms filterlim_cong by (force 10 4)

lemma continuous_at_within_cong:
  assumes "f x = g x" "eventually (λx. f x = g x) (at x within S)"
  shows "continuous (at x within S) f ⟷ continuous (at x within S) g"
  using assms by (simp add: continuous_within filterlim_cong)

lemma tendsto_power_int [tendsto_intros]:
  fixes a :: "'a::real_normed_div_algebra"
  assumes f: "(f ⤏ a) F"
    and a: "a ≠ 0"
  shows "((λx. power_int (f x) n) ⤏ power_int a n) F"
  using assms by (cases n rule: int_cases4) (auto intro!: tendsto_intros simp: power_int_minus)

lemma continuous_power_int:
  fixes f :: "'a::t2_space ⇒ 'b::real_normed_div_algebra"
  assumes "continuous F f"
    and "f (Lim F (λx. x)) ≠ 0"
  shows "continuous F (λx. power_int (f x) n)"
  using assms unfolding continuous_def by (rule tendsto_power_int)

lemma continuous_at_within_power_int[continuous_intros]:
  fixes f :: "'a::t2_space ⇒ 'b::real_normed_div_algebra"
  assumes "continuous (at a within s) f"
    and "f a ≠ 0"
  shows "continuous (at a within s) (λx. power_int (f x) n)"
  using assms unfolding continuous_within by (rule tendsto_power_int)

lemma continuous_on_power_int [continuous_intros]:
  fixes f :: "'a::topological_space ⇒ 'b::real_normed_div_algebra"
  assumes "continuous_on s f" and "n ≥ 0 ∨ (∀x∈s. f x ≠ 0)"
  shows "continuous_on s (λx. power_int (f x) n)"
  using assms by (cases "n ≥ 0") (auto simp: power_int_def intro!: continuous_intros)

lemma tendsto_power_int' [tendsto_intros]:
  fixes a :: "'a::real_normed_div_algebra"
  assumes f: "(f ⤏ a) F"
    and a: "a ≠ 0 ∨ n ≥ 0"
  shows "((λx. power_int (f x) n) ⤏ power_int a n) F"
  using assms by (cases n rule: int_cases4) (auto intro!: tendsto_intros simp: power_int_minus)

lemma tendsto_sgn [tendsto_intros]: "(f ⤏ l) F ⟹ l ≠ 0 ⟹ ((λx. sgn (f x)) ⤏ sgn l) F"
  for l :: "'a::real_normed_vector"
  unfolding sgn_div_norm by (simp add: tendsto_intros)

lemma continuous_sgn:
  fixes f :: "'a::t2_space ⇒ 'b::real_normed_vector"
  assumes "continuous F f"
    and "f (Lim F (λx. x)) ≠ 0"
  shows "continuous F (λx. sgn (f x))"
  using assms unfolding continuous_def by (rule tendsto_sgn)

lemma continuous_at_within_sgn[continuous_intros]:
  fixes f :: "'a::t2_space ⇒ 'b::real_normed_vector"
  assumes "continuous (at a within s) f"
    and "f a ≠ 0"
  shows "continuous (at a within s) (λx. sgn (f x))"
  using assms unfolding continuous_within by (rule tendsto_sgn)

lemma isCont_sgn[continuous_intros]:
  fixes f :: "'a::t2_space ⇒ 'b::real_normed_vector"
  assumes "isCont f a"
    and "f a ≠ 0"
  shows "isCont (λx. sgn (f x)) a"
  using assms unfolding continuous_at by (rule tendsto_sgn)

lemma continuous_on_sgn[continuous_intros]:
  fixes f :: "'a::topological_space ⇒ 'b::real_normed_vector"
  assumes "continuous_on s f"
    and "∀x∈s. f x ≠ 0"
  shows "continuous_on s (λx. sgn (f x))"
  using assms unfolding continuous_on_def by (blast intro: tendsto_sgn)

lemma filterlim_at_infinity:
  fixes f :: "_ ⇒ 'a::real_normed_vector"
  assumes "0 ≤ c"
  shows "(LIM x F. f x :> at_infinity) ⟷ (∀r>c. eventually (λx. r ≤ norm (f x)) F)"
  unfolding filterlim_iff eventually_at_infinity
proof safe
  fix P :: "'a ⇒ bool"
  fix b
  assume *: "∀r>c. eventually (λx. r ≤ norm (f x)) F"
  assume P: "∀x. b ≤ norm x ⟶ P x"
  have "max b (c + 1) > c" by auto
  with * have "eventually (λx. max b (c + 1) ≤ norm (f x)) F"
    by auto
  then show "eventually (λx. P (f x)) F"
  proof eventually_elim
    case (elim x)
    with P show "P (f x)" by auto
  qed
qed force

lemma filterlim_at_infinity_imp_norm_at_top:
  fixes F
  assumes "filterlim f at_infinity F"
  shows   "filterlim (λx. norm (f x)) at_top F"
proof -
  {
    fix r :: real
    have "∀⇩F x in F. r ≤ norm (f x)" using filterlim_at_infinity[of 0 f F] assms
      by (cases "r > 0")
         (auto simp: not_less intro: always_eventually order.trans[OF _ norm_ge_zero])
  }
  thus ?thesis by (auto simp: filterlim_at_top)
qed

lemma filterlim_norm_at_top_imp_at_infinity:
  fixes F
  assumes "filterlim (λx. norm (f x)) at_top F"
  shows   "filterlim f at_infinity F"
  using filterlim_at_infinity[of 0 f F] assms by (auto simp: filterlim_at_top)

lemma filterlim_norm_at_top: "filterlim norm at_top at_infinity"
  by (rule filterlim_at_infinity_imp_norm_at_top) (rule filterlim_ident)

lemma filterlim_at_infinity_conv_norm_at_top:
  "filterlim f at_infinity G ⟷ filterlim (λx. norm (f x)) at_top G"
  by (auto simp: filterlim_at_infinity[OF order.refl] filterlim_at_top_gt[of _ _ 0])

lemma eventually_not_equal_at_infinity:
  "eventually (λx. x ≠ (a :: 'a :: {real_normed_vector})) at_infinity"
proof -
  from filterlim_norm_at_top[where 'a = 'a]
    have "∀⇩F x in at_infinity. norm a < norm (x::'a)" by (auto simp: filterlim_at_top_dense)
  thus ?thesis by eventually_elim auto
qed

lemma filterlim_int_of_nat_at_topD:
  fixes F
  assumes "filterlim (λx. f (int x)) F at_top"
  shows   "filterlim f F at_top"
proof -
  have "filterlim (λx. f (int (nat x))) F at_top"
    by (rule filterlim_compose[OF assms filterlim_nat_sequentially])
  also have "?this ⟷ filterlim f F at_top"
    by (intro filterlim_cong refl eventually_mono [OF eventually_ge_at_top[of "0::int"]]) auto
  finally show ?thesis .
qed

lemma filterlim_int_sequentially [tendsto_intros]:
  "filterlim int at_top sequentially"
  unfolding filterlim_at_top
proof
  fix C :: int
  show "eventually (λn. int n ≥ C) at_top"
    using eventually_ge_at_top[of "nat ⌈C⌉"] by eventually_elim linarith
qed

lemma filterlim_real_of_int_at_top [tendsto_intros]:
  "filterlim real_of_int at_top at_top"
  unfolding filterlim_at_top
proof
  fix C :: real
  show "eventually (λn. real_of_int n ≥ C) at_top"
    using eventually_ge_at_top[of "⌈C⌉"] by eventually_elim linarith
qed

lemma filterlim_abs_real: "filterlim (abs::real ⇒ real) at_top at_top"
proof (subst filterlim_cong[OF refl refl])
  from eventually_ge_at_top[of "0::real"] show "eventually (λx::real. ¦x¦ = x) at_top"
    by eventually_elim simp
qed (simp_all add: filterlim_ident)

lemma filterlim_of_real_at_infinity [tendsto_intros]:
  "filterlim (of_real :: real ⇒ 'a :: real_normed_algebra_1) at_infinity at_top"
  by (intro filterlim_norm_at_top_imp_at_infinity) (auto simp: filterlim_abs_real)

lemma not_tendsto_and_filterlim_at_infinity:
  fixes c :: "'a::real_normed_vector"
  assumes "F ≠ bot"
    and "(f ⤏ c) F"
    and "filterlim f at_infinity F"
  shows False
proof -
  from tendstoD[OF assms(2), of "1/2"]
  have "eventually (λx. dist (f x) c < 1/2) F"
    by simp
  moreover
  from filterlim_at_infinity[of "norm c" f F] assms(3)
  have "eventually (λx. norm (f x) ≥ norm c + 1) F" by simp
  ultimately have "eventually (λx. False) F"
  proof eventually_elim
    fix x
    assume A: "dist (f x) c < 1/2"
    assume "norm (f x) ≥ norm c + 1"
    also have "norm (f x) = dist (f x) 0" by simp
    also have "… ≤ dist (f x) c + dist c 0" by (rule dist_triangle)
    finally show False using A by simp
  qed
  with assms show False by simp
qed

lemma filterlim_at_infinity_imp_not_convergent:
  assumes "filterlim f at_infinity sequentially"
  shows "¬ convergent f"
  by (rule notI, rule not_tendsto_and_filterlim_at_infinity[OF _ _ assms])
     (simp_all add: convergent_LIMSEQ_iff)

lemma filterlim_at_infinity_imp_eventually_ne:
  assumes "filterlim f at_infinity F"
  shows "eventually (λz. f z ≠ c) F"
proof -
  have "norm c + 1 > 0"
    by (intro add_nonneg_pos) simp_all
  with filterlim_at_infinity[OF order.refl, of f F] assms
  have "eventually (λz. norm (f z) ≥ norm c + 1) F"
    by blast
  then show ?thesis
    by eventually_elim auto
qed

lemma tendsto_of_nat [tendsto_intros]:
  "filterlim (of_nat :: nat ⇒ 'a::real_normed_algebra_1) at_infinity sequentially"
proof (subst filterlim_at_infinity[OF order.refl], intro allI impI)
  fix r :: real
  assume r: "r > 0"
  define n where "n = nat ⌈r⌉"
  from r have n: "∀m≥n. of_nat m ≥ r"
    unfolding n_def by linarith
  from eventually_ge_at_top[of n] show "eventually (λm. norm (of_nat m :: 'a) ≥ r) sequentially"
    by eventually_elim (use n in simp_all)
qed


subsection ‹Relate \<^const>‹at›, \<^const>‹at_left› and \<^const>‹at_right››

text ‹
  This lemmas are useful for conversion between \<^term>‹at x› to \<^term>‹at_left x› and
  \<^term>‹at_right x› and also \<^term>‹at_right 0›.
›

lemmas filterlim_split_at_real = filterlim_split_at[where 'a=real]

lemma filtermap_nhds_shift: "filtermap (λx. x - d) (nhds a) = nhds (a - d)"
  for a d :: "'a::real_normed_vector"
  by (rule filtermap_fun_inverse[where g="λx. x + d"])
    (auto intro!: tendsto_eq_intros filterlim_ident)

lemma filtermap_nhds_minus: "filtermap (λx. - x) (nhds a) = nhds (- a)"
  for a :: "'a::real_normed_vector"
  by (rule filtermap_fun_inverse[where g=uminus])
    (auto intro!: tendsto_eq_intros filterlim_ident)

lemma filtermap_at_shift: "filtermap (λx. x - d) (at a) = at (a - d)"
  for a d :: "'a::real_normed_vector"
  by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_shift[symmetric])

lemma filtermap_at_right_shift: "filtermap (λx. x - d) (at_right a) = at_right (a - d)"
  for a d :: "real"
  by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_shift[symmetric])

lemma filterlim_shift:
  fixes d :: "'a::real_normed_vector"
  assumes "filterlim f F (at a)"
  shows "filterlim (f ∘ (+) d) F (at (a - d))"
  unfolding filterlim_iff
proof (intro strip)
  fix P
  assume "eventually P F"
  then have "∀⇩F x in filtermap (λy. y - d) (at a). P (f (d + x))"
    using assms by (force simp add: filterlim_iff eventually_filtermap)
  then show "(∀⇩F x in at (a - d). P ((f ∘ (+) d) x))"
    by (force simp add: filtermap_at_shift)
qed

lemma filterlim_shift_iff:
  fixes d :: "'a::real_normed_vector"
  shows "filterlim (f ∘ (+) d) F (at (a - d)) = filterlim f F (at a)"   (is "?lhs = ?rhs")
proof
  assume L: ?lhs show ?rhs
    using filterlim_shift [OF L, of "-d"] by (simp add: filterlim_iff)
qed (metis filterlim_shift)

lemma at_right_to_0: "at_right a = filtermap (λx. x + a) (at_right 0)"
  for a :: real
  using filtermap_at_right_shift[of "-a" 0] by simp

lemma filterlim_at_right_to_0:
  "filterlim f F (at_right a) ⟷ filterlim (λx. f (x + a)) F (at_right 0)"
  for a :: real
  unfolding filterlim_def filtermap_filtermap at_right_to_0[of a] ..

lemma eventually_at_right_to_0:
  "eventually P (at_right a) ⟷ eventually (λx. P (x + a)) (at_right 0)"
  for a :: real
  unfolding at_right_to_0[of a] by (simp add: eventually_filtermap)

lemma at_to_0: "at a = filtermap (λx. x + a) (at 0)"
  for a :: "'a::real_normed_vector"
  using filtermap_at_shift[of "-a" 0] by simp

lemma filterlim_at_to_0:
  "filterlim f F (at a) ⟷ filterlim (λx. f (x + a)) F (at 0)"
  for a :: "'a::real_normed_vector"
  unfolding filterlim_def filtermap_filtermap at_to_0[of a] ..

lemma eventually_at_to_0:
  "eventually P (at a) ⟷ eventually (λx. P (x + a)) (at 0)"
  for a ::  "'a::real_normed_vector"
  unfolding at_to_0[of a] by (simp add: eventually_filtermap)

lemma filtermap_at_minus: "filtermap (λx. - x) (at a) = at (- a)"
  for a :: "'a::real_normed_vector"
  by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric])

lemma at_left_minus: "at_left a = filtermap (λx. - x) (at_right (- a))"
  for a :: real
  by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric])

lemma at_right_minus: "at_right a = filtermap (λx. - x) (at_left (- a))"
  for a :: real
  by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric])

lemma filtermap_linear_at_within:
  assumes "bij f" and cont: "isCont f a" and open_map: "⋀S. open S ⟹ open (f`S)"
  shows "filtermap f (at a within S) = at (f a) within f`S"
  unfolding filter_eq_iff
proof safe
  fix P
  assume "eventually P (filtermap f (at a within S))"
  then obtain T where "open T" "a ∈ T" and impP:"∀x∈T. x≠a ⟶ x∈S⟶ P (f x)"
    by (auto simp: eventually_filtermap eventually_at_topological)
  then show "eventually P (at (f a) within f ` S)"
    unfolding eventually_at_topological
    apply (intro exI[of _ "f`T"])
    using ‹bij f› open_map by (metis bij_pointE image_iff)
next
  fix P
  assume "eventually P (at (f a) within f ` S)"
  then obtain T1 where "open T1" "f a ∈ T1" and impP:"∀x∈T1. x≠f a ⟶ x∈f`S⟶ P (x)"
    unfolding eventually_at_topological by auto
  then obtain T2 where "open T2" "a ∈ T2" "(∀x'∈T2. f x' ∈ T1)"
    using cont[unfolded continuous_at_open,rule_format,of T1] by blast
  then have "∀x∈T2. x≠a ⟶ x∈S⟶ P (f x)"
    using impP by (metis assms(1) bij_pointE imageI)
  then show "eventually P (filtermap f (at a within S))"
    unfolding eventually_filtermap eventually_at_topological
    apply (intro exI[of _ T2])
    using ‹open T2› ‹a ∈ T2› by auto
qed

lemma filterlim_at_left_to_right:
  "filterlim f F (at_left a) ⟷ filterlim (λx. f (- x)) F (at_right (-a))"
  for a :: real
  unfolding filterlim_def filtermap_filtermap at_left_minus[of a] ..

lemma eventually_at_left_to_right:
  "eventually P (at_left a) ⟷ eventually (λx. P (- x)) (at_right (-a))"
  for a :: real
  unfolding at_left_minus[of a] by (simp add: eventually_filtermap)

lemma filterlim_uminus_at_top_at_bot: "LIM x at_bot. - x :: real :> at_top"
  unfolding filterlim_at_top eventually_at_bot_dense
  by (metis leI minus_less_iff order_less_asym)

lemma filterlim_uminus_at_bot_at_top: "LIM x at_top. - x :: real :> at_bot"
  unfolding filterlim_at_bot eventually_at_top_dense
  by (metis leI less_minus_iff order_less_asym)

lemma at_bot_mirror :
  shows "(at_bot::('a::{ordered_ab_group_add,linorder} filter)) = filtermap uminus at_top"
proof (rule filtermap_fun_inverse[symmetric])
  show "filterlim uminus at_top (at_bot::'a filter)"
    using eventually_at_bot_linorder filterlim_at_top le_minus_iff
    (*NEW*)
    by (force run exec: "Zip.Depth_First.all 5")
    (*ORIG*)
    (* by force+ *)
  show "filterlim uminus (at_bot::'a filter) at_top"
    by (simp add: filterlim_at_bot minus_le_iff)
qed auto

lemma at_top_mirror :
  shows "(at_top::('a::{ordered_ab_group_add,linorder} filter)) = filtermap uminus at_bot"
  apply (subst at_bot_mirror)
  by (auto simp: filtermap_filtermap)

lemma filterlim_at_top_mirror: "(LIM x at_top. f x :> F) ⟷ (LIM x at_bot. f (-x::real) :> F)"
  unfolding filterlim_def at_top_mirror filtermap_filtermap ..

lemma filterlim_at_bot_mirror: "(LIM x at_bot. f x :> F) ⟷ (LIM x at_top. f (-x::real) :> F)"
  unfolding filterlim_def at_bot_mirror filtermap_filtermap ..

lemma filterlim_uminus_at_top: "(LIM x F. f x :> at_top) ⟷ (LIM x F. - (f x) :: real :> at_bot)"
  using filterlim_compose[OF filterlim_uminus_at_bot_at_top, of f F]
    and filterlim_compose[OF filterlim_uminus_at_top_at_bot, of "λx. - f x" F]
  by auto

lemma tendsto_at_botI_sequentially:
  fixes f :: "real ⇒ 'b::first_countable_topology"
  assumes *: "⋀X. filterlim X at_bot sequentially ⟹ (λn. f (X n)) ⇢ y"
  shows "(f ⤏ y) at_bot"
  unfolding filterlim_at_bot_mirror
proof (rule tendsto_at_topI_sequentially)
  fix X :: "nat ⇒ real" assume "filterlim X at_top sequentially"
  thus "(λn. f (-X n)) ⇢ y" by (intro *) (auto simp: filterlim_uminus_at_top)
qed

lemma filterlim_at_infinity_imp_filterlim_at_top:
  assumes "filterlim (f :: 'a ⇒ real) at_infinity F"
  assumes "eventually (λx. f x > 0) F"
  shows   "filterlim f at_top F"
proof -
  from assms(2) have *: "eventually (λx. norm (f x) = f x) F" by eventually_elim simp
  from assms(1) show ?thesis unfolding filterlim_at_infinity_conv_norm_at_top
    by (subst (asm) filterlim_cong[OF refl refl *])
qed

lemma filterlim_at_infinity_imp_filterlim_at_bot:
  assumes "filterlim (f :: 'a ⇒ real) at_infinity F"
  assumes "eventually (λx. f x < 0) F"
  shows   "filterlim f at_bot F"
proof -
  from assms(2) have *: "eventually (λx. norm (f x) = -f x) F" by eventually_elim simp
  from assms(1) have "filterlim (λx. - f x) at_top F"
    unfolding filterlim_at_infinity_conv_norm_at_top
    by (subst (asm) filterlim_cong[OF refl refl *])
  thus ?thesis by (simp add: filterlim_uminus_at_top)
qed

lemma filterlim_uminus_at_bot: "(LIM x F. f x :> at_bot) ⟷ (LIM x F. - (f x) :: real :> at_top)"
  unfolding filterlim_uminus_at_top by simp

lemma filterlim_inverse_at_top_right: "LIM x at_right (0::real). inverse x :> at_top"
  unfolding filterlim_at_top_gt[where c=0] eventually_at_filter
proof safe
  fix Z :: real
  assume [arith]: "0 < Z"
  then have "eventually (λx. x < inverse Z) (nhds 0)"
    by (auto simp: eventually_nhds_metric dist_real_def intro!: exI[of _ "¦inverse Z¦"])
  then show "eventually (λx. x ≠ 0 ⟶ x ∈ {0<..} ⟶ Z ≤ inverse x) (nhds 0)"
    by (auto elim!: eventually_mono simp: inverse_eq_divide field_simps)
qed

lemma tendsto_inverse_0:
  fixes x :: "_ ⇒ 'a::real_normed_div_algebra"
  shows "(inverse ⤏ (0::'a)) at_infinity"
  unfolding tendsto_Zfun_iff diff_0_right Zfun_def eventually_at_infinity
proof safe
  fix r :: real
  assume "0 < r"
  show "∃b. ∀x. b ≤ norm x ⟶ norm (inverse x :: 'a) < r"
  proof (intro exI[of _ "inverse (r / 2)"] allI impI)
    fix x :: 'a
    from ‹0 < r› have "0 < inverse (r / 2)" by simp
    also assume *: "inverse (r / 2) ≤ norm x"
    finally show "norm (inverse x) < r"
      using * ‹0 < r›
      by (subst nonzero_norm_inverse) (simp_all add: inverse_eq_divide field_simps)
  qed
qed

lemma tendsto_add_filterlim_at_infinity:
  fixes c :: "'b::real_normed_vector"
    and F :: "'a filter"
  assumes "(f ⤏ c) F"
    and "filterlim g at_infinity F"
  shows "filterlim (λx. f x + g x) at_infinity F"
proof (subst filterlim_at_infinity[OF order_refl], safe)
  fix r :: real
  assume r: "r > 0"
  from assms(1) have "((λx. norm (f x)) ⤏ norm c) F"
    by (rule tendsto_norm)
  then have "eventually (λx. norm (f x) < norm c + 1) F"
    by (rule order_tendstoD) simp_all
  moreover from r have "r + norm c + 1 > 0"
    by (intro add_pos_nonneg) simp_all
  with assms(2) have "eventually (λx. norm (g x) ≥ r + norm c + 1) F"
    unfolding filterlim_at_infinity[OF order_refl]
    by (elim allE[of _ "r + norm c + 1"]) simp_all
  ultimately show "eventually (λx. norm (f x + g x) ≥ r) F"
  proof eventually_elim
    fix x :: 'a
    assume A: "norm (f x) < norm c + 1" and B: "r + norm c + 1 ≤ norm (g x)"
    from A B have "r ≤ norm (g x) - norm (f x)"
      by simp
    also have "norm (g x) - norm (f x) ≤ norm (g x + f x)"
      by (rule norm_diff_ineq)
    finally show "r ≤ norm (f x + g x)"
      by (simp add: add_ac)
  qed
qed

lemma tendsto_add_filterlim_at_infinity':
  fixes c :: "'b::real_normed_vector"
    and F :: "'a filter"
  assumes "filterlim f at_infinity F"
    and "(g ⤏ c) F"
  shows "filterlim (λx. f x + g x) at_infinity F"
  by (subst add.commute) (rule tendsto_add_filterlim_at_infinity assms)+

lemma filterlim_inverse_at_right_top: "LIM x at_top. inverse x :> at_right (0::real)"
  unfolding filterlim_at
  (*NOTE keep original non-terminal auto call for reproducibility*)
  by (auto_orig simp: eventually_at_top_dense)
     (metis tendsto_inverse_0 filterlim_mono at_top_le_at_infinity order_refl)

lemma filterlim_inverse_at_top:
  "(f ⤏ (0 :: real)) F ⟹ eventually (λx. 0 < f x) F ⟹ LIM x F. inverse (f x) :> at_top"
  by (intro filterlim_compose[OF filterlim_inverse_at_top_right])
     (simp add: filterlim_def eventually_filtermap eventually_mono at_within_def le_principal)

lemma filterlim_inverse_at_bot_neg:
  "LIM x (at_left (0::real)). inverse x :> at_bot"
  by (simp add: filterlim_inverse_at_top_right filterlim_uminus_at_bot filterlim_at_left_to_right)

lemma filterlim_inverse_at_bot:
  "(f ⤏ (0 :: real)) F ⟹ eventually (λx. f x < 0) F ⟹ LIM x F. inverse (f x) :> at_bot"
  unfolding filterlim_uminus_at_bot inverse_minus_eq[symmetric]
  by (rule filterlim_inverse_at_top) (simp_all add: tendsto_minus_cancel_left[symmetric])

lemma at_right_to_top: "(at_right (0::real)) = filtermap inverse at_top"
  by (intro filtermap_fun_inverse[symmetric, where g=inverse])
     (auto intro: filterlim_inverse_at_top_right filterlim_inverse_at_right_top)

lemma eventually_at_right_to_top:
  "eventually P (at_right (0::real)) ⟷ eventually (λx. P (inverse x)) at_top"
  unfolding at_right_to_top eventually_filtermap ..

lemma filterlim_at_right_to_top:
  "filterlim f F (at_right (0::real)) ⟷ (LIM x at_top. f (inverse x) :> F)"
  unfolding filterlim_def at_right_to_top filtermap_filtermap ..

lemma at_top_to_right: "at_top = filtermap inverse (at_right (0::real))"
  unfolding at_right_to_top filtermap_filtermap inverse_inverse_eq filtermap_ident ..

lemma eventually_at_top_to_right:
  "eventually P at_top ⟷ eventually (λx. P (inverse x)) (at_right (0::real))"
  unfolding at_top_to_right eventually_filtermap ..

lemma filterlim_at_top_to_right:
  "filterlim f F at_top ⟷ (LIM x (at_right (0::real)). f (inverse x) :> F)"
  unfolding filterlim_def at_top_to_right filtermap_filtermap ..

lemma filterlim_inverse_at_infinity:
  fixes x :: "_ ⇒ 'a::{real_normed_div_algebra, division_ring}"
  shows "filterlim inverse at_infinity (at (0::'a))"
  unfolding filterlim_at_infinity[OF order_refl]
proof safe
  fix r :: real
  assume "0 < r"
  then show "eventually (λx::'a. r ≤ norm (inverse x)) (at 0)"
    unfolding eventually_at norm_inverse
    by (intro exI[of _ "inverse r"])
       (auto simp: norm_conv_dist[symmetric] field_simps inverse_eq_divide)
qed

lemma filterlim_inverse_at_iff:
  fixes g :: "'a ⇒ 'b::{real_normed_div_algebra, division_ring}"
  shows "(LIM x F. inverse (g x) :> at 0) ⟷ (LIM x F. g x :> at_infinity)"
  unfolding filterlim_def filtermap_filtermap[symmetric]
proof
  assume "filtermap g F ≤ at_infinity"
  then have "filtermap inverse (filtermap g F) ≤ filtermap inverse at_infinity"
    by (rule filtermap_mono)
  also have "… ≤ at 0"
    using tendsto_inverse_0[where 'a='b]
    by (auto intro!: exI[of _ 1]
        simp: le_principal eventually_filtermap filterlim_def at_within_def eventually_at_infinity)
  finally show "filtermap inverse (filtermap g F) ≤ at 0" .
next
  assume "filtermap inverse (filtermap g F) ≤ at 0"
  then have "filtermap inverse (filtermap inverse (filtermap g F)) ≤ filtermap inverse (at 0)"
    by (rule filtermap_mono)
  with filterlim_inverse_at_infinity show "filtermap g F ≤ at_infinity"
    by (auto intro: order_trans simp: filterlim_def filtermap_filtermap)
qed

lemma tendsto_mult_filterlim_at_infinity:
  fixes c :: "'a::real_normed_field"
  assumes  "(f ⤏ c) F" "c ≠ 0"
  assumes "filterlim g at_infinity F"
  shows "filterlim (λx. f x * g x) at_infinity F"
proof -
  have "((λx. inverse (f x) * inverse (g x)) ⤏ inverse c * 0) F"
    by (intro tendsto_mult tendsto_inverse assms filterlim_compose[OF tendsto_inverse_0])
  then have "filterlim (λx. inverse (f x) * inverse (g x)) (at (inverse c * 0)) F"
    unfolding filterlim_at
    using assms
    by (auto intro: filterlim_at_infinity_imp_eventually_ne tendsto_imp_eventually_ne eventually_conj)
  then show ?thesis
    by (subst filterlim_inverse_at_iff[symmetric]) simp_all
qed

lemma filterlim_power_int_neg_at_infinity:
  fixes f :: "_ ⇒ 'a::{real_normed_div_algebra, division_ring}"
  assumes "n < 0" and lim: "(f ⤏ 0) F" and ev: "eventually (λx. f x ≠ 0) F"
  shows   "filterlim (λx. f x powi n) at_infinity F"
proof -
  have lim': "((λx. f x ^ nat (- n)) ⤏ 0) F"
    by (rule tendsto_eq_intros lim)+ (use ‹n < 0› in auto)
  have ev': "eventually (λx. f x ^ nat (-n) ≠ 0) F"
    using ev by eventually_elim (use ‹n < 0› in auto)
  have "filterlim (λx. inverse (f x ^ nat (-n))) at_infinity F"
    by (intro filterlim_compose[OF filterlim_inverse_at_infinity])
       (use lim' ev' in ‹auto simp: filterlim_at›)
  thus ?thesis
    using ‹n < 0› by (simp add: power_int_def power_inverse)
qed

lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top ⟹ ((λx. inverse (f x) :: real) ⤏ 0) F"
  by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff)

lemma filterlim_inverse_at_top_iff:
  "eventually (λx. 0 < f x) F ⟹ (LIM x F. inverse (f x) :> at_top) ⟷ (f ⤏ (0 :: real)) F"
  by (auto dest: tendsto_inverse_0_at_top filterlim_inverse_at_top)

lemma filterlim_at_top_iff_inverse_0:
  "eventually (λx. 0 < f x) F ⟹ (LIM x F. f x :> at_top) ⟷ ((inverse ∘ f) ⤏ (0 :: real)) F"
  using filterlim_inverse_at_top_iff [of "inverse ∘ f"] by auto

lemma real_tendsto_divide_at_top:
  fixes c::"real"
  assumes "(f ⤏ c) F"
  assumes "filterlim g at_top F"
  shows "((λx. f x / g x) ⤏ 0) F"
  by (auto simp: divide_inverse_commute
      intro!: tendsto_mult[THEN tendsto_eq_rhs] tendsto_inverse_0_at_top assms)

lemma mult_nat_left_at_top: "c > 0 ⟹ filterlim (λx. c * x) at_top sequentially"
  for c :: nat
  by (rule filterlim_subseq) (auto simp: strict_mono_def)

lemma mult_nat_right_at_top: "c > 0 ⟹ filterlim (λx. x * c) at_top sequentially"
  for c :: nat
  by (rule filterlim_subseq) (auto simp: strict_mono_def)

lemma filterlim_times_pos:
  "LIM x F1. c * f x :> at_right l"
  if "filterlim f (at_right p) F1" "0 < c" "l = c * p"
  for c::"'a::{linordered_field, linorder_topology}"
  unfolding filterlim_iff
proof safe
  fix P
  assume "∀⇩F x in at_right l. P x"
  then obtain d where "c * p < d" "⋀y. y > c * p ⟹ y < d ⟹ P y"
    unfolding ‹l = _ › eventually_at_right_field
    by auto
  then have "∀⇩F a in at_right p. P (c * a)"
    by (auto simp: eventually_at_right_field ‹0 < c› field_simps intro!: exI[where x="d/c"])
  from that(1)[unfolded filterlim_iff, rule_format, OF this]
  show "∀⇩F x in F1. P (c * f x)" .
qed

lemma filtermap_nhds_times: "c ≠ 0 ⟹ filtermap (times c) (nhds a) = nhds (c * a)"
  for a c :: "'a::real_normed_field"
  by (rule filtermap_fun_inverse[where g="λx. inverse c * x"])
    (auto intro!: tendsto_eq_intros filterlim_ident)

lemma filtermap_times_pos_at_right:
  fixes c::"'a::{linordered_field, linorder_topology}"
  assumes "c > 0"
  shows "filtermap (times c) (at_right p) = at_right (c * p)"
  using assms
  by (intro filtermap_fun_inverse[where g="λx. inverse c * x"])
    (auto intro!: filterlim_ident filterlim_times_pos)

lemma at_to_infinity: "(at (0::'a::{real_normed_field,field})) = filtermap inverse at_infinity"
proof (rule antisym)
  have "(inverse ⤏ (0::'a)) at_infinity"
    by (fact tendsto_inverse_0)
  then show "filtermap inverse at_infinity ≤ at (0::'a)"
    using filterlim_def filterlim_ident filterlim_inverse_at_iff
    (*NEW*)
    by (fastforce run exec: Zip.Depth_First.all')
    (*ORIG*)
    (* by (fastforce) *)
next
  have "filtermap inverse (filtermap inverse (at (0::'a))) ≤ filtermap inverse at_infinity"
    using filterlim_inverse_at_infinity unfolding filterlim_def
    by (rule filtermap_mono)
  then show "at (0::'a) ≤ filtermap inverse at_infinity"
    by (simp add: filtermap_ident filtermap_filtermap)
qed

lemma lim_at_infinity_0:
  fixes l :: "'a::{real_normed_field,field}"
  shows "(f ⤏ l) at_infinity ⟷ ((f ∘ inverse) ⤏ l) (at (0::'a))"
  by (simp add: tendsto_compose_filtermap at_to_infinity filtermap_filtermap)

lemma lim_zero_infinity:
  fixes l :: "'a::{real_normed_field,field}"
  shows "((λx. f(1 / x)) ⤏ l) (at (0::'a)) ⟹ (f ⤏ l) at_infinity"
  by (simp add: inverse_eq_divide lim_at_infinity_0 comp_def)


text ‹
  We only show rules for multiplication and addition when the functions are either against a real
  value or against infinity. Further rules are easy to derive by using @{thm
  filterlim_uminus_at_top}.
›

lemma filterlim_tendsto_pos_mult_at_top:
  assumes f: "(f ⤏ c) F"
    and c: "0 < c"
    and g: "LIM x F. g x :> at_top"
  shows "LIM x F. (f x * g x :: real) :> at_top"
  unfolding filterlim_at_top_gt[where c=0]
proof safe
  fix Z :: real
  assume "0 < Z"
  from f ‹0 < c› have "eventually (λx. c / 2 < f x) F"
    by (auto dest!: tendstoD[where e="c / 2"] elim!: eventually_mono
        simp: dist_real_def abs_real_def split: if_split_asm)
  moreover from g have "eventually (λx. (Z / c * 2) ≤ g x) F"
    unfolding filterlim_at_top by auto
  ultimately show "eventually (λx. Z ≤ f x * g x) F"
  proof eventually_elim
    case (elim x)
    with ‹0 < Z› ‹0 < c› have "c / 2 * (Z / c * 2) ≤ f x * g x"
      by (intro mult_mono) (auto simp: zero_le_divide_iff)
    with ‹0 < c› show "Z ≤ f x * g x"
       by simp
  qed
qed

lemma filterlim_at_top_mult_at_top:
  assumes f: "LIM x F. f x :> at_top"
    and g: "LIM x F. g x :> at_top"
  shows "LIM x F. (f x * g x :: real) :> at_top"
  unfolding filterlim_at_top_gt[where c=0]
proof safe
  fix Z :: real
  assume "0 < Z"
  from f have "eventually (λx. 1 ≤ f x) F"
    unfolding filterlim_at_top by auto
  moreover from g have "eventually (λx. Z ≤ g x) F"
    unfolding filterlim_at_top by auto
  ultimately show "eventually (λx. Z ≤ f x * g x) F"
  proof eventually_elim
    case (elim x)
    with ‹0 < Z› have "1 * Z ≤ f x * g x"
      by (intro mult_mono) (auto simp: zero_le_divide_iff)
    then show "Z ≤ f x * g x"
       by simp
  qed
qed

lemma filterlim_at_top_mult_tendsto_pos:
  assumes f: "(f ⤏ c) F"
    and c: "0 < c"
    and g: "LIM x F. g x :> at_top"
  shows "LIM x F. (g x * f x:: real) :> at_top"
  by (auto simp: mult.commute intro!: filterlim_tendsto_pos_mult_at_top f c g)

lemma filterlim_tendsto_pos_mult_at_bot:
  fixes c :: real
  assumes "(f ⤏ c) F" "0 < c" "filterlim g at_bot F"
  shows "LIM x F. f x * g x :> at_bot"
  using filterlim_tendsto_pos_mult_at_top[OF assms(1,2), of "λx. - g x"] assms(3)
  unfolding filterlim_uminus_at_bot by simp

lemma filterlim_tendsto_neg_mult_at_bot:
  fixes c :: real
  assumes c: "(f ⤏ c) F" "c < 0" and g: "filterlim g at_top F"
  shows "LIM x F. f x * g x :> at_bot"
  using c filterlim_tendsto_pos_mult_at_top[of "λx. - f x" "- c" F, OF _ _ g]
  unfolding filterlim_uminus_at_bot tendsto_minus_cancel_left by simp


lemma filterlim_cmult_at_bot_at_top:
  assumes "filterlim (h :: _ ⇒ real) at_top F" "c ≠ 0" "G = (if c > 0 then at_top else at_bot)"
  shows   "filterlim (λx. c * h x) G F"
  using assms filterlim_tendsto_pos_mult_at_top[OF tendsto_const[of c], of h F]
              filterlim_tendsto_neg_mult_at_bot[OF tendsto_const[of c], of h F] by simp

lemma filterlim_pow_at_top:
  fixes f :: "'a ⇒ real"
  assumes "0 < n"
    and f: "LIM x F. f x :> at_top"
  shows "LIM x F. (f x)^n :: real :> at_top"
  using ‹0 < n›
proof (induct n)
  case 0
  then show ?case by simp
next
  case (Suc n) with f show ?case
    by (cases "n = 0") (auto intro!: filterlim_at_top_mult_at_top)
qed

lemma filterlim_pow_at_bot_even:
  fixes f :: "real ⇒ real"
  shows "0 < n ⟹ LIM x F. f x :> at_bot ⟹ even n ⟹ LIM x F. (f x)^n :> at_top"
  using filterlim_pow_at_top[of n "λx. - f x" F] by (simp add: filterlim_uminus_at_top)

lemma filterlim_pow_at_bot_odd:
  fixes f :: "real ⇒ real"
  shows "0 < n ⟹ LIM x F. f x :> at_bot ⟹ odd n ⟹ LIM x F. (f x)^n :> at_bot"
  using filterlim_pow_at_top[of n "λx. - f x" F] by (simp add: filterlim_uminus_at_bot)

lemma filterlim_power_at_infinity [tendsto_intros]:
  fixes F and f :: "'a ⇒ 'b :: real_normed_div_algebra"
  assumes "filterlim f at_infinity F" "n > 0"
  shows   "filterlim (λx. f x ^ n) at_infinity F"
  by (rule filterlim_norm_at_top_imp_at_infinity)
     (auto simp: norm_power intro!: filterlim_pow_at_top assms
           intro: filterlim_at_infinity_imp_norm_at_top)

lemma filterlim_tendsto_add_at_top:
  assumes f: "(f ⤏ c) F"
    and g: "LIM x F. g x :> at_top"
  shows "LIM x F. (f x + g x :: real) :> at_top"
  unfolding filterlim_at_top_gt[where c=0]
proof safe
  fix Z :: real
  assume "0 < Z"
  from f have "eventually (λx. c - 1 < f x) F"
    by (auto dest!: tendstoD[where e=1] elim!: eventually_mono simp: dist_real_def)
  moreover from g have "eventually (λx. Z - (c - 1) ≤ g x) F"
    unfolding filterlim_at_top by auto
  ultimately show "eventually (λx. Z ≤ f x + g x) F"
    by eventually_elim simp
qed

lemma filterlim_tendsto_add_at_top_iff:
  assumes f: "(f ⤏ c) F"
  shows "(LIM x F. (f x + g x :: real) :> at_top) ⟷ (LIM x F. g x :> at_top)"
proof
  assume "LIM x F. f x + g x :> at_top"
  moreover have "((λx. - f x) ⤏ - c) F"
    by (simp add: f tendsto_minus)
  ultimately show "filterlim g at_top F"
    using filterlim_tendsto_add_at_top
    (*NEW*)
    by (fastforce where run exec: Zip.Depth_First.all')
    (*ORIG*)
    (* by (fastforce) *)
qed (auto simp: filterlim_tendsto_add_at_top[OF f])

lemma filterlim_tendsto_add_at_bot_iff:
  fixes c::real
  assumes f: "(f ⤏ c) F"
  shows "(LIM x F. f x + g x :> at_bot) ⟷ (LIM x F. g x :> at_bot)"
proof -
  have "(LIM x F. f x + g x :> at_bot)
        ⟷  (LIM x F. - f x + (- g x)  :> at_top)"
    by (simp add: filterlim_uminus_at_bot)
  also have "... = (LIM x F. - g x  :> at_top)"
    by (metis f filterlim_tendsto_add_at_top_iff tendsto_minus)
  also have "... = (LIM x F. g x  :> at_bot)"
    by (simp add: filterlim_uminus_at_bot)
  finally show ?thesis .
qed

lemma LIM_at_top_divide:
  fixes f g :: "'a ⇒ real"
  assumes f: "(f ⤏ a) F" "0 < a"
    and g: "(g ⤏ 0) F" "eventually (λx. 0 < g x) F"
  shows "LIM x F. f x / g x :> at_top"
  unfolding divide_inverse
  by (rule filterlim_tendsto_pos_mult_at_top[OF f]) (rule filterlim_inverse_at_top[OF g])

lemma filterlim_at_top_add_at_top:
  assumes f: "LIM x F. f x :> at_top"
    and g: "LIM x F. g x :> at_top"
  shows "LIM x F. (f x + g x :: real) :> at_top"
  unfolding filterlim_at_top_gt[where c=0]
proof safe
  fix Z :: real
  assume "0 < Z"
  from f have "eventually (λx. 0 ≤ f x) F"
    unfolding filterlim_at_top by auto
  moreover from g have "eventually (λx. Z ≤ g x) F"
    unfolding filterlim_at_top by auto
  ultimately show "eventually (λx. Z ≤ f x + g x) F"
    by eventually_elim simp
qed

lemma tendsto_divide_0:
  fixes f :: "_ ⇒ 'a::{real_normed_div_algebra, division_ring}"
  assumes f: "(f ⤏ c) F"
    and g: "LIM x F. g x :> at_infinity"
  shows "((λx. f x / g x) ⤏ 0) F"
  using tendsto_mult[OF f filterlim_compose[OF tendsto_inverse_0 g]]
  by (simp add: divide_inverse)

lemma linear_plus_1_le_power:
  fixes x :: real
  assumes x: "0 ≤ x"
  shows "real n * x + 1 ≤ (x + 1) ^ n"
proof (induct n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  from x have "real (Suc n) * x + 1 ≤ (x + 1) * (real n * x + 1)"
    by (simp add: field_simps)
  also have "… ≤ (x + 1)^Suc n"
    using Suc x by (simp add: mult_left_mono)
  finally show ?case .
qed

lemma filterlim_realpow_sequentially_gt1:
  fixes x :: "'a :: real_normed_div_algebra"
  assumes x[arith]: "1 < norm x"
  shows "LIM n sequentially. x ^ n :> at_infinity"
proof (intro filterlim_at_infinity[THEN iffD2] allI impI)
  fix y :: real
  assume "0 < y"
  obtain N :: nat where "y < real N * (norm x - 1)"
    by (meson diff_gt_0_iff_gt reals_Archimedean3 x)
  also have "… ≤ real N * (norm x - 1) + 1"
    by simp
  also have "… ≤ (norm x - 1 + 1) ^ N"
    by (rule linear_plus_1_le_power) simp
  also have "… = norm x ^ N"
    by simp
  finally have "∀n≥N. y ≤ norm x ^ n"
    by (metis order_less_le_trans power_increasing order_less_imp_le x)
  then show "eventually (λn. y ≤ norm (x ^ n)) sequentially"
    unfolding eventually_sequentially
    by (auto simp: norm_power)
qed simp


lemma filterlim_divide_at_infinity:
  fixes f g :: "'a ⇒ 'a :: real_normed_field"
  assumes "filterlim f (nhds c) F" "filterlim g (at 0) F" "c ≠ 0"
  shows   "filterlim (λx. f x / g x) at_infinity F"
proof -
  have "filterlim (λx. f x * inverse (g x)) at_infinity F"
    by (intro tendsto_mult_filterlim_at_infinity[OF assms(1,3)]
          filterlim_compose [OF filterlim_inverse_at_infinity assms(2)])
  thus ?thesis by (simp add: field_simps)
qed

subsection ‹Floor and Ceiling›

lemma eventually_floor_less:
  fixes f :: "'a ⇒ 'b::{order_topology,floor_ceiling}"
  assumes f: "(f ⤏ l) F"
    and l: "l ∉ ℤ"
  shows "∀⇩F x in F. of_int (floor l) < f x"
  by (intro order_tendstoD[OF f]) (metis Ints_of_int antisym_conv2 floor_correct l)

lemma eventually_less_ceiling:
  fixes f :: "'a ⇒ 'b::{order_topology,floor_ceiling}"
  assumes f: "(f ⤏ l) F"
    and l: "l ∉ ℤ"
  shows "∀⇩F x in F. f x < of_int (ceiling l)"
  by (intro order_tendstoD[OF f]) (metis Ints_of_int l le_of_int_ceiling less_le)

lemma eventually_floor_eq:
  fixes f::"'a ⇒ 'b::{order_topology,floor_ceiling}"
  assumes f: "(f ⤏ l) F"
    and l: "l ∉ ℤ"
  shows "∀⇩F x in F. floor (f x) = floor l"
  using eventually_floor_less[OF assms] eventually_less_ceiling[OF assms]
  by eventually_elim (meson floor_less_iff less_ceiling_iff not_less_iff_gr_or_eq)

lemma eventually_ceiling_eq:
  fixes f::"'a ⇒ 'b::{order_topology,floor_ceiling}"
  assumes f: "(f ⤏ l) F"
    and l: "l ∉ ℤ"
  shows "∀⇩F x in F. ceiling (f x) = ceiling l"
  using eventually_floor_less[OF assms] eventually_less_ceiling[OF assms]
  by eventually_elim (meson floor_less_iff less_ceiling_iff not_less_iff_gr_or_eq)

lemma tendsto_of_int_floor:
  fixes f::"'a ⇒ 'b::{order_topology,floor_ceiling}"
  assumes "(f ⤏ l) F"
    and "l ∉ ℤ"
  shows "((λx. of_int (floor (f x)) :: 'c::{ring_1,topological_space}) ⤏ of_int (floor l)) F"
  using eventually_floor_eq[OF assms]
  by (simp add: eventually_mono topological_tendstoI)

lemma tendsto_of_int_ceiling:
  fixes f::"'a ⇒ 'b::{order_topology,floor_ceiling}"
  assumes "(f ⤏ l) F"
    and "l ∉ ℤ"
  shows "((λx. of_int (ceiling (f x)):: 'c::{ring_1,topological_space}) ⤏ of_int (ceiling l)) F"
  using eventually_ceiling_eq[OF assms]
  by (simp add: eventually_mono topological_tendstoI)

lemma continuous_on_of_int_floor:
  "continuous_on (UNIV - ℤ::'a::{order_topology, floor_ceiling} set)
    (λx. of_int (floor x)::'b::{ring_1, topological_space})"
  unfolding continuous_on_def
  by (auto intro!: tendsto_of_int_floor)

lemma continuous_on_of_int_ceiling:
  "continuous_on (UNIV - ℤ::'a::{order_topology, floor_ceiling} set)
    (λx. of_int (ceiling x)::'b::{ring_1, topological_space})"
  unfolding continuous_on_def
  by (auto intro!: tendsto_of_int_ceiling)


subsection ‹Limits of Sequences›

lemma [trans]: "X = Y ⟹ Y ⇢ z ⟹ X ⇢ z"
  by simp

lemma LIMSEQ_iff:
  fixes L :: "'a::real_normed_vector"
  shows "(X ⇢ L) = (∀r>0. ∃no. ∀n ≥ no. norm (X n - L) < r)"
unfolding lim_sequentially dist_norm ..

lemma LIMSEQ_I: "(⋀r. 0 < r ⟹ ∃no. ∀n≥no. norm (X n - L) < r) ⟹ X ⇢ L"
  for L :: "'a::real_normed_vector"
  by (simp add: LIMSEQ_iff)

lemma LIMSEQ_D: "X ⇢ L ⟹ 0 < r ⟹ ∃no. ∀n≥no. norm (X n - L) < r"
  for L :: "'a::real_normed_vector"
  by (simp add: LIMSEQ_iff)

lemma LIMSEQ_linear: "X ⇢ x ⟹ l > 0 ⟹ (λ n. X (n * l)) ⇢ x"
  unfolding tendsto_def eventually_sequentially
  by (metis div_le_dividend div_mult_self1_is_m le_trans mult.commute)


text ‹Transformation of limit.›

lemma Lim_transform: "(g ⤏ a) F ⟹ ((λx. f x - g x) ⤏ 0) F ⟹ (f ⤏ a) F"
  for a b :: "'a::real_normed_vector"
  using tendsto_add [of g a F "λx. f x - g x" 0] by simp

lemma Lim_transform2: "(f ⤏ a) F ⟹ ((λx. f x - g x) ⤏ 0) F ⟹ (g ⤏ a) F"
  for a b :: "'a::real_normed_vector"
  by (erule Lim_transform) (simp add: tendsto_minus_cancel)

proposition Lim_transform_eq: "((λx. f x - g x) ⤏ 0) F ⟹ (f ⤏ a) F ⟷ (g ⤏ a) F"
  for a :: "'a::real_normed_vector"
  using Lim_transform Lim_transform2 by blast

lemma Lim_transform_eventually:
  "⟦(f ⤏ l) F; eventually (λx. f x = g x) F⟧ ⟹ (g ⤏ l) F"
  using eventually_elim2
  (*NEW*)
  by (fastforce simp add: tendsto_def where run exec: Zip.Depth_First.all')
  (*ORIG*)
  (* by (fastforce simp add: tendsto_def) *)

lemma Lim_transform_within:
  assumes "(f ⤏ l) (at x within S)"
    and "0 < d"
    and "⋀x'. x'∈S ⟹ 0 < dist x' x ⟹ dist x' x < d ⟹ f x' = g x'"
  shows "(g ⤏ l) (at x within S)"
proof (rule Lim_transform_eventually)
  show "eventually (λx. f x = g x) (at x within S)"
    using assms by (auto simp: eventually_at)
  show "(f ⤏ l) (at x within S)"
    by fact
qed

lemma filterlim_transform_within:
  assumes "filterlim g G (at x within S)"
  assumes "G ≤ F" "0<d" "(⋀x'. x' ∈ S ⟹ 0 < dist x' x ⟹ dist x' x < d ⟹ f x' = g x') "
  shows "filterlim f F (at x within S)"
  using assms
  apply (elim filterlim_mono_eventually)
  unfolding eventually_at by auto

text ‹Common case assuming being away from some crucial point like 0.›
lemma Lim_transform_away_within:
  fixes a b :: "'a::t1_space"
  assumes "a ≠ b"
    and "∀x∈S. x ≠ a ∧ x ≠ b ⟶ f x = g x"
    and "(f ⤏ l) (at a within S)"
  shows "(g ⤏ l) (at a within S)"
proof (rule Lim_transform_eventually)
  show "(f ⤏ l) (at a within S)"
    by fact
  show "eventually (λx. f x = g x) (at a within S)"
    unfolding eventually_at_topological
    by (rule exI [where x="- {b}"]) (simp add: open_Compl assms)
qed

lemma Lim_transform_away_at:
  fixes a b :: "'a::t1_space"
  assumes ab: "a ≠ b"
    and fg: "∀x. x ≠ a ∧ x ≠ b ⟶ f x = g x"
    and fl: "(f ⤏ l) (at a)"
  shows "(g ⤏ l) (at a)"
  using Lim_transform_away_within[OF ab, of UNIV f g l] fg fl by simp

text ‹Alternatively, within an open set.›
lemma Lim_transform_within_open:
  assumes "(f ⤏ l) (at a within T)"
    and "open s" and "a ∈ s"
    and "⋀x. x∈s ⟹ x ≠ a ⟹ f x = g x"
  shows "(g ⤏ l) (at a within T)"
proof (rule Lim_transform_eventually)
  show "eventually (λx. f x = g x) (at a within T)"
    unfolding eventually_at_topological
    using assms by auto
  show "(f ⤏ l) (at a within T)" by fact
qed


text ‹A congruence rule allowing us to transform limits assuming not at point.›

lemma Lim_cong_within:
  assumes "a = b"
    and "x = y"
    and "S = T"
    and "⋀x. x ≠ b ⟹ x ∈ T ⟹ f x = g x"
  shows "(f ⤏ x) (at a within S) ⟷ (g ⤏ y) (at b within T)"
  unfolding tendsto_def eventually_at_topological
  using assms by simp

text ‹An unbounded sequence's inverse tends to 0.›
lemma LIMSEQ_inverse_zero:
  assumes "⋀r::real. ∃N. ∀n≥N. r < X n"
  shows "(λn. inverse (X n)) ⇢ 0"
  apply (rule filterlim_compose[OF tendsto_inverse_0])
  by (metis assms eventually_at_top_linorderI filterlim_at_top_dense filterlim_at_top_imp_at_infinity)

text ‹The sequence \<^term>‹1/n› tends to 0 as \<^term>‹n› tends to infinity.›
lemma LIMSEQ_inverse_real_of_nat: "(λn. inverse (real (Suc n))) ⇢ 0"
  by (metis filterlim_compose tendsto_inverse_0 filterlim_mono order_refl filterlim_Suc
      filterlim_compose[OF filterlim_real_sequentially] at_top_le_at_infinity)

text ‹
  The sequence \<^term>‹r + 1/n› tends to \<^term>‹r› as \<^term>‹n› tends to
  infinity is now easily proved.
›

lemma LIMSEQ_inverse_real_of_nat_add: "(λn. r + inverse (real (Suc n))) ⇢ r"
  using tendsto_add [OF tendsto_const LIMSEQ_inverse_real_of_nat] by auto

lemma LIMSEQ_inverse_real_of_nat_add_minus: "(λn. r + -inverse (real (Suc n))) ⇢ r"
  using tendsto_add [OF tendsto_const tendsto_minus [OF LIMSEQ_inverse_real_of_nat]]
  by auto

lemma LIMSEQ_inverse_real_of_nat_add_minus_mult: "(λn. r * (1 + - inverse (real (Suc n)))) ⇢ r"
  using tendsto_mult [OF tendsto_const LIMSEQ_inverse_real_of_nat_add_minus [of 1]]
  by auto

lemma lim_inverse_n: "((λn. inverse(of_nat n)) ⤏ (0::'a::real_normed_field)) sequentially"
  using lim_1_over_n by (simp add: inverse_eq_divide)

lemma lim_inverse_n': "((λn. 1 / n) ⤏ 0) sequentially"
  using lim_inverse_n
  by (simp add: inverse_eq_divide)

lemma LIMSEQ_Suc_n_over_n: "(λn. of_nat (Suc n) / of_nat n :: 'a :: real_normed_field) ⇢ 1"
proof (rule Lim_transform_eventually)
  show "eventually (λn. 1 + inverse (of_nat n :: 'a) = of_nat (Suc n) / of_nat n) sequentially"
    using eventually_gt_at_top[of "0::nat"]
    by eventually_elim (simp add: field_simps)
  have "(λn. 1 + inverse (of_nat n) :: 'a) ⇢ 1 + 0"
    by (intro tendsto_add tendsto_const lim_inverse_n)
  then show "(λn. 1 + inverse (of_nat n) :: 'a) ⇢ 1"
    by simp
qed

lemma LIMSEQ_n_over_Suc_n: "(λn. of_nat n / of_nat (Suc n) :: 'a :: real_normed_field) ⇢ 1"
proof (rule Lim_transform_eventually)
  show "eventually (λn. inverse (of_nat (Suc n) / of_nat n :: 'a) =
      of_nat n / of_nat (Suc n)) sequentially"
    using eventually_gt_at_top[of "0::nat"]
    by eventually_elim (simp add: field_simps del: of_nat_Suc)
  have "(λn. inverse (of_nat (Suc n) / of_nat n :: 'a)) ⇢ inverse 1"
    by (intro tendsto_inverse LIMSEQ_Suc_n_over_n) simp_all
  then show "(λn. inverse (of_nat (Suc n) / of_nat n :: 'a)) ⇢ 1"
    by simp
qed


subsection ‹Convergence on sequences›

lemma convergent_cong:
  assumes "eventually (λx. f x = g x) sequentially"
  shows "convergent f ⟷ convergent g"
  unfolding convergent_def
  by (subst filterlim_cong[OF refl refl assms]) (rule refl)

lemma convergent_Suc_iff: "convergent (λn. f (Suc n)) ⟷ convergent f"
  by (auto simp: convergent_def filterlim_sequentially_Suc)

lemma convergent_ignore_initial_segment: "convergent (λn. f (n + m)) = convergent f"
proof (induct m arbitrary: f)
  case 0
  then show ?case by simp
next
  case (Suc m)
  have "convergent (λn. f (n + Suc m)) ⟷ convergent (λn. f (Suc n + m))"
    by simp
  also have "… ⟷ convergent (λn. f (n + m))"
    by (rule convergent_Suc_iff)
  also have "… ⟷ convergent f"
    by (rule Suc)
  finally show ?case .
qed

lemma convergent_add:
  fixes X Y :: "nat ⇒ 'a::topological_monoid_add"
  assumes "convergent (λn. X n)"
    and "convergent (λn. Y n)"
  shows "convergent (λn. X n + Y n)"
  using assms unfolding convergent_def by (blast intro: tendsto_add)

lemma convergent_sum:
  fixes X :: "'a ⇒ nat ⇒ 'b::topological_comm_monoid_add"
  shows "(⋀i. i ∈ A ⟹ convergent (λn. X i n)) ⟹ convergent (λn. ∑i∈A. X i n)"
  by (induct A rule: infinite_finite_induct) (simp_all add: convergent_const convergent_add)

lemma (in bounded_linear) convergent:
  assumes "convergent (λn. X n)"
  shows "convergent (λn. f (X n))"
  using assms unfolding convergent_def by (blast intro: tendsto)

lemma (in bounded_bilinear) convergent:
  assumes "convergent (λn. X n)"
    and "convergent (λn. Y n)"
  shows "convergent (λn. X n ** Y n)"
  using assms unfolding convergent_def by (blast intro: tendsto)

lemma convergent_minus_iff:
  fixes X :: "nat ⇒ 'a::topological_group_add"
  shows "convergent X ⟷ convergent (λn. - X n)"
  unfolding convergent_def by (force 0 4 dest: tendsto_minus)

lemma convergent_diff:
  fixes X Y :: "nat ⇒ 'a::topological_group_add"
  assumes "convergent (λn. X n)"
  assumes "convergent (λn. Y n)"
  shows "convergent (λn. X n - Y n)"
  using assms unfolding convergent_def by (blast intro: tendsto_diff)

lemma convergent_norm:
  assumes "convergent f"
  shows "convergent (λn. norm (f n))"
proof -
  from assms have "f ⇢ lim f"
    by (simp add: convergent_LIMSEQ_iff)
  then have "(λn. norm (f n)) ⇢ norm (lim f)"
    by (rule tendsto_norm)
  then show ?thesis
    by (auto simp: convergent_def)
qed

lemma convergent_of_real:
  "convergent f ⟹ convergent (λn. of_real (f n) :: 'a::real_normed_algebra_1)"
  unfolding convergent_def by (blast intro!: tendsto_of_real)

lemma convergent_add_const_iff:
  "convergent (λn. c + f n :: 'a::topological_ab_group_add) ⟷ convergent f"
proof
  assume "convergent (λn. c + f n)"
  from convergent_diff[OF this convergent_const[of c]] show "convergent f"
    by simp
next
  assume "convergent f"
  from convergent_add[OF convergent_const[of c] this] show "convergent (λn. c + f n)"
    by simp
qed

lemma convergent_add_const_right_iff:
  "convergent (λn. f n + c :: 'a::topological_ab_group_add) ⟷ convergent f"
  using convergent_add_const_iff[of c f] by (simp add: add_ac)

lemma convergent_diff_const_right_iff:
  "convergent (λn. f n - c :: 'a::topological_ab_group_add) ⟷ convergent f"
  using convergent_add_const_right_iff[of f "-c"] by (simp add: add_ac)

lemma convergent_mult:
  fixes X Y :: "nat ⇒ 'a::topological_semigroup_mult"
  assumes "convergent (λn. X n)"
    and "convergent (λn. Y n)"
  shows "convergent (λn. X n * Y n)"
  using assms unfolding convergent_def by (blast intro: tendsto_mult)

lemma convergent_mult_const_iff:
  assumes "c ≠ 0"
  shows "convergent (λn. c * f n :: 'a::{field,topological_semigroup_mult}) ⟷ convergent f"
proof
  assume "convergent (λn. c * f n)"
  from assms convergent_mult[OF this convergent_const[of "inverse c"]]
    show "convergent f" by (simp add: field_simps)
next
  assume "convergent f"
  from convergent_mult[OF convergent_const[of c] this] show "convergent (λn. c * f n)"
    by simp
qed

lemma convergent_mult_const_right_iff:
  fixes c :: "'a::{field,topological_semigroup_mult}"
  assumes "c ≠ 0"
  shows "convergent (λn. f n * c) ⟷ convergent f"
  using convergent_mult_const_iff[OF assms, of f] by (simp add: mult_ac)

lemma convergent_imp_Bseq: "convergent f ⟹ Bseq f"
  by (simp add: Cauchy_Bseq convergent_Cauchy)


text ‹A monotone sequence converges to its least upper bound.›

lemma LIMSEQ_incseq_SUP:
  fixes X :: "nat ⇒ 'a::{conditionally_complete_linorder,linorder_topology}"
  assumes u: "bdd_above (range X)"
    and X: "incseq X"
  shows "X ⇢ (SUP i. X i)"
  by (rule order_tendstoI)
    (auto simp: eventually_sequentially u less_cSUP_iff
      intro: X[THEN incseqD] less_le_trans cSUP_lessD[OF u])

lemma LIMSEQ_decseq_INF:
  fixes X :: "nat ⇒ 'a::{conditionally_complete_linorder, linorder_topology}"
  assumes u: "bdd_below (range X)"
    and X: "decseq X"
  shows "X ⇢ (INF i. X i)"
  by (rule order_tendstoI)
     (auto simp: eventually_sequentially u cINF_less_iff
       intro: X[THEN decseqD] le_less_trans less_cINF_D[OF u])

text ‹Main monotonicity theorem.›

lemma Bseq_monoseq_convergent: "Bseq X ⟹ monoseq X ⟹ convergent X"
  for X :: "nat ⇒ real"
  by (auto simp: monoseq_iff convergent_def intro: LIMSEQ_decseq_INF LIMSEQ_incseq_SUP
      dest: Bseq_bdd_above Bseq_bdd_below)

lemma Bseq_mono_convergent: "Bseq X ⟹ (∀m n. m ≤ n ⟶ X m ≤ X n) ⟹ convergent X"
  for X :: "nat ⇒ real"
  by (auto intro!: Bseq_monoseq_convergent incseq_imp_monoseq simp: incseq_def)

lemma monoseq_imp_convergent_iff_Bseq: "monoseq f ⟹ convergent f ⟷ Bseq f"
  for f :: "nat ⇒ real"
  using Bseq_monoseq_convergent[of f] convergent_imp_Bseq[of f] by blast

lemma Bseq_monoseq_convergent'_inc:
  fixes f :: "nat ⇒ real"
  shows "Bseq (λn. f (n + M)) ⟹ (⋀m n. M ≤ m ⟹ m ≤ n ⟹ f m ≤ f n) ⟹ convergent f"
  by (subst convergent_ignore_initial_segment [symmetric, of _ M])
     (auto intro!: Bseq_monoseq_convergent simp: monoseq_def)

lemma Bseq_monoseq_convergent'_dec:
  fixes f :: "nat ⇒ real"
  shows "Bseq (λn. f (n + M)) ⟹ (⋀m n. M ≤ m ⟹ m ≤ n ⟹ f m ≥ f n) ⟹ convergent f"
  by (subst convergent_ignore_initial_segment [symmetric, of _ M])
    (auto intro!: Bseq_monoseq_convergent simp: monoseq_def)

lemma Cauchy_iff: "Cauchy X ⟷ (∀e>0. ∃M. ∀m≥M. ∀n≥M. norm (X m - X n) < e)"
  for X :: "nat ⇒ 'a::real_normed_vector"
  unfolding Cauchy_def dist_norm ..

lemma CauchyI: "(⋀e. 0 < e ⟹ ∃M. ∀m≥M. ∀n≥M. norm (X m - X n) < e) ⟹ Cauchy X"
  for X :: "nat ⇒ 'a::real_normed_vector"
  by (simp add: Cauchy_iff)

lemma CauchyD: "Cauchy X ⟹ 0 < e ⟹ ∃M. ∀m≥M. ∀n≥M. norm (X m - X n) < e"
  for X :: "nat ⇒ 'a::real_normed_vector"
  by (simp add: Cauchy_iff)

lemma incseq_convergent:
  fixes X :: "nat ⇒ real"
  assumes "incseq X"
    and "∀i. X i ≤ B"
  obtains L where "X ⇢ L" "∀i. X i ≤ L"
proof atomize_elim
  from incseq_bounded[OF assms] ‹incseq X› Bseq_monoseq_convergent[of X]
  obtain L where "X ⇢ L"
    by (auto simp: convergent_def monoseq_def incseq_def)
  with ‹incseq X› show "∃L. X ⇢ L ∧ (∀i. X i ≤ L)"
    by (auto intro!: exI[of _ L] incseq_le)
qed

lemma decseq_convergent:
  fixes X :: "nat ⇒ real"
  assumes "decseq X"
    and "∀i. B ≤ X i"
  obtains L where "X ⇢ L" "∀i. L ≤ X i"
proof atomize_elim
  from decseq_bounded[OF assms] ‹decseq X› Bseq_monoseq_convergent[of X]
  obtain L where "X ⇢ L"
    by (auto simp: convergent_def monoseq_def decseq_def)
  with ‹decseq X› show "∃L. X ⇢ L ∧ (∀i. L ≤ X i)"
    by (auto intro!: exI[of _ L] decseq_ge)
qed

lemma monoseq_convergent:
  fixes X :: "nat ⇒ real"
  assumes X: "monoseq X" and B: "⋀i. ¦X i¦ ≤ B"
  obtains L where "X ⇢ L"
  using X unfolding monoseq_iff
proof
  assume "incseq X"
  show thesis
    using abs_le_D1 [OF B] incseq_convergent [OF ‹incseq X›] that by meson
next
  assume "decseq X"
  show thesis
    using decseq_convergent [OF ‹decseq X›] that
    by (metis B abs_le_iff add.inverse_inverse neg_le_iff_le)
qed

subsection ‹More about @{term filterlim} (thanks to Wenda Li)›

lemma filterlim_at_infinity_times:
  fixes f :: "'a ⇒ 'b::real_normed_field"
  assumes "filterlim f at_infinity F" "filterlim g at_infinity F"
  shows "filterlim (λx. f x * g x) at_infinity F"
proof -
  have "((λx. inverse (f x) * inverse (g x)) ⤏ 0 * 0) F"
    by (intro tendsto_mult tendsto_inverse assms filterlim_compose[OF tendsto_inverse_0])
  then have "filterlim (λx. inverse (f x) * inverse (g x)) (at 0) F"
    unfolding filterlim_at using assms
    by (auto intro: filterlim_at_infinity_imp_eventually_ne tendsto_imp_eventually_ne eventually_conj)
  then show ?thesis
    by (subst filterlim_inverse_at_iff[symmetric]) simp_all
qed

lemma filterlim_at_top_at_bot[elim]:
  fixes f::"'a ⇒ 'b::unbounded_dense_linorder" and F::"'a filter"
  assumes top:"filterlim f at_top F" and bot: "filterlim f at_bot F" and "F≠bot"
  shows False
proof -
  obtain c::'b where True by auto
  have "∀⇩F x in F. c < f x"
    using top unfolding filterlim_at_top_dense by auto
  moreover have "∀⇩F x in F. f x < c"
    using bot unfolding filterlim_at_bot_dense by auto
  ultimately have "∀⇩F x in F. c < f x ∧ f x < c"
    using eventually_conj by auto
  then have "∀⇩F x in F. False" by (auto elim:eventually_mono)
  then show False using ‹F≠bot› by auto
qed

lemma filterlim_at_top_nhds[elim]:
  fixes f::"'a ⇒ 'b::{unbounded_dense_linorder,order_topology}" and F::"'a filter"
  assumes top:"filterlim f at_top F" and tendsto: "(f ⤏ c) F" and "F≠bot"
  shows False
proof -
  obtain c'::'b where "c'>c" using gt_ex by blast
  have "∀⇩F x in F. c' < f x"
    using top unfolding filterlim_at_top_dense by auto
  moreover have "∀⇩F x in F. f x < c'"
    using order_tendstoD[OF tendsto,of c'] ‹c'>c› by auto
  ultimately have "∀⇩F x in F. c' < f x ∧ f x < c'"
    using eventually_conj by auto
  then have "∀⇩F x in F. False" by (auto elim:eventually_mono)
  then show False using ‹F≠bot› by auto
qed

lemma filterlim_at_bot_nhds[elim]:
  fixes f::"'a ⇒ 'b::{unbounded_dense_linorder,order_topology}" and F::"'a filter"
  assumes top:"filterlim f at_bot F" and tendsto: "(f ⤏ c) F" and "F≠bot"
  shows False
proof -
  obtain c'::'b where "c'<c" using lt_ex by blast
  have "∀⇩F x in F. c' > f x"
    using top unfolding filterlim_at_bot_dense by auto
  moreover have "∀⇩F x in F. f x > c'"
    using order_tendstoD[OF tendsto,of c'] ‹c'<c› by auto
  ultimately have "∀⇩F x in F. c' < f x ∧ f x < c'"
    using eventually_conj by auto
  then have "∀⇩F x in F. False" by (auto elim:eventually_mono)
  then show False using ‹F≠bot› by auto
qed

lemma eventually_times_inverse_1:
  fixes f::"'a ⇒ 'b::{field,t2_space}"
  assumes "(f ⤏ c) F" "c≠0"
  shows "∀⇩F x in F. inverse (f x) * f x = 1"
  by (smt (verit) assms eventually_mono mult.commute right_inverse tendsto_imp_eventually_ne)

lemma filterlim_at_infinity_divide_iff:
  fixes f::"'a ⇒ 'b::real_normed_field"
  assumes "(f ⤏ c) F" "c≠0"
  shows "(LIM x F. f x / g x :> at_infinity) ⟷ (LIM x F. g x :> at 0)"
proof
  assume "LIM x F. f x / g x :> at_infinity"
  then have "LIM x F. inverse (f x) * (f x / g x) :> at_infinity"
    using assms tendsto_inverse tendsto_mult_filterlim_at_infinity
      (*NEW*)
      by (fastforce run exec: Zip.Depth_First.all')
      (*ORIG*)
      (* by fastforce+ *)
  then have "LIM x F. inverse (g x) :> at_infinity"
    apply (elim filterlim_mono_eventually)
    using eventually_times_inverse_1[OF assms]
    by (auto elim:eventually_mono simp add:field_simps)
  then show "filterlim g (at 0) F" using filterlim_inverse_at_iff[symmetric] by (force)
next
  assume "filterlim g (at 0) F"
  then have "filterlim (λx. inverse (g x)) at_infinity F"
    using filterlim_compose filterlim_inverse_at_infinity by blast
  then have "LIM x F. f x * inverse (g x) :> at_infinity"
    using tendsto_mult_filterlim_at_infinity[OF assms, of "λx. inverse(g x)"]
    by simp
  then show "LIM x F. f x / g x :> at_infinity" by (simp add: divide_inverse)
qed

lemma filterlim_tendsto_pos_mult_at_top_iff:
  fixes f::"'a ⇒ real"
  assumes "(f ⤏ c) F" and "0 < c"
  shows "(LIM x F. (f x * g x) :> at_top) ⟷ (LIM x F. g x :> at_top)"
proof
  assume "filterlim g at_top F"
  then show "LIM x F. f x * g x :> at_top"
    using filterlim_tendsto_pos_mult_at_top[OF assms] by auto
next
  assume asm:"LIM x F. f x * g x :> at_top"
  have "((λx. inverse (f x)) ⤏ inverse c) F"
    using tendsto_inverse[OF assms(1)] ‹0<c› by auto
  moreover have "inverse c >0" using assms(2) by auto
  ultimately have "LIM x F. inverse (f x) * (f x * g x) :> at_top"
    using filterlim_tendsto_pos_mult_at_top[OF _ _ asm,of "λx. inverse (f x)" "inverse c"] by auto
  then show "LIM x F. g x :> at_top"
    apply (elim filterlim_mono_eventually)
      apply simp_all[2]
    using eventually_times_inverse_1[OF assms(1)] ‹c>0› eventually_mono by (fastforce)
qed

lemma filterlim_tendsto_pos_mult_at_bot_iff:
  fixes c :: real
  assumes "(f ⤏ c) F" "0 < c"
  shows "(LIM x F. f x * g x :> at_bot) ⟷ filterlim g at_bot F"
  using filterlim_tendsto_pos_mult_at_top_iff[OF assms(1,2), of "λx. - g x"]
  unfolding filterlim_uminus_at_bot by simp

lemma filterlim_tendsto_neg_mult_at_top_iff:
  fixes f::"'a ⇒ real"
  assumes "(f ⤏ c) F" and "c < 0"
  shows "(LIM x F. (f x * g x) :> at_top) ⟷ (LIM x F. g x :> at_bot)"
proof -
  have "(LIM x F. f x * g x :> at_top) = (LIM x F. - g x :> at_top)"
    apply (rule filterlim_tendsto_pos_mult_at_top_iff[of "λx. - f x" "-c" F "λx. - g x", simplified])
    using assms by (auto intro: tendsto_intros )
  also have "... = (LIM x F. g x :> at_bot)"
    using filterlim_uminus_at_bot[symmetric] by auto
  finally show ?thesis .
qed

lemma filterlim_tendsto_neg_mult_at_bot_iff:
  fixes c :: real
  assumes "(f ⤏ c) F" "0 > c"
  shows "(LIM x F. f x * g x :> at_bot) ⟷ filterlim g at_top F"
  using filterlim_tendsto_neg_mult_at_top_iff[OF assms(1,2), of "λx. - g x"]
  unfolding filterlim_uminus_at_top by simp

subsection ‹Power Sequences›

lemma Bseq_realpow: "0 ≤ x ⟹ x ≤ 1 ⟹ Bseq (λn. x ^ n)"
  for x :: real
  by (metis decseq_bounded decseq_def power_decreasing zero_le_power)

lemma monoseq_realpow: "0 ≤ x ⟹ x ≤ 1 ⟹ monoseq (λn. x ^ n)"
  for x :: real
  using monoseq_def power_decreasing by blast

lemma convergent_realpow: "0 ≤ x ⟹ x ≤ 1 ⟹ convergent (λn. x ^ n)"
  for x :: real
  by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow)

lemma LIMSEQ_inverse_realpow_zero: "1 < x ⟹ (λn. inverse (x ^ n)) ⇢ 0"
  for x :: real
  by (rule filterlim_compose[OF tendsto_inverse_0 filterlim_realpow_sequentially_gt1]) simp

lemma LIMSEQ_realpow_zero:
  fixes x :: real
  assumes "0 ≤ x" "x < 1"
  shows "(λn. x ^ n) ⇢ 0"
proof (cases "x = 0")
  case False
  with ‹0 ≤ x› have "1 < inverse x"
    using ‹x < 1› by (simp add: one_less_inverse)
  then have "(λn. inverse (inverse x ^ n)) ⇢ 0"
    by (rule LIMSEQ_inverse_realpow_zero)
  then show ?thesis by (simp add: power_inverse)
next
  case True
  show ?thesis
    by (rule LIMSEQ_imp_Suc) (simp add: True)
qed

lemma LIMSEQ_power_zero [tendsto_intros]: "norm x < 1 ⟹ (λn. x ^ n) ⇢ 0"
  for x :: "'a::real_normed_algebra_1"
  apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero])
  by (simp add: Zfun_le norm_power_ineq tendsto_Zfun_iff)

lemma LIMSEQ_divide_realpow_zero: "1 < x ⟹ (λn. a / (x ^ n) :: real) ⇢ 0"
  by (rule tendsto_divide_0 [OF tendsto_const filterlim_realpow_sequentially_gt1]) simp

lemma
  tendsto_power_zero:
  fixes x::"'a::real_normed_algebra_1"
  assumes "filterlim f at_top F"
  assumes "norm x < 1"
  shows "((λy. x ^ (f y)) ⤏ 0) F"
proof (rule tendstoI)
  fix e::real assume "0 < e"
  from tendstoD[OF LIMSEQ_power_zero[OF ‹norm x < 1›] ‹0 < e›]
  have "∀⇩F xa in sequentially. norm (x ^ xa) < e"
    by simp
  then obtain N where N: "norm (x ^ n) < e" if "n ≥ N" for n
    by (auto simp: eventually_sequentially)
  have "∀⇩F i in F. f i ≥ N"
    using ‹filterlim f sequentially F›
    by (simp add: filterlim_at_top)
  then show "∀⇩F i in F. dist (x ^ f i) 0 < e"
    by eventually_elim (auto simp: N)
qed

text ‹Limit of \<^term>‹c^n› for \<^term>‹¦c¦ < 1›.›

lemma LIMSEQ_abs_realpow_zero: "¦c¦ < 1 ⟹ (λn. ¦c¦ ^ n :: real) ⇢ 0"
  by (rule LIMSEQ_realpow_zero [OF abs_ge_zero])

lemma LIMSEQ_abs_realpow_zero2: "¦c¦ < 1 ⟹ (λn. c ^ n :: real) ⇢ 0"
  by (rule LIMSEQ_power_zero) simp


subsection ‹Limits of Functions›

lemma LIM_eq: "f ─a→ L = (∀r>0. ∃s>0. ∀x. x ≠ a ∧ norm (x - a) < s ⟶ norm (f x - L) < r)"
  for a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
  by (simp add: LIM_def dist_norm)

lemma LIM_I:
  "(⋀r. 0 < r ⟹ ∃s>0. ∀x. x ≠ a ∧ norm (x - a) < s ⟶ norm (f x - L) < r) ⟹ f ─a→ L"
  for a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
  by (simp add: LIM_eq)

lemma LIM_D: "f ─a→ L ⟹ 0 < r ⟹ ∃s>0.∀x. x ≠ a ∧ norm (x - a) < s ⟶ norm (f x - L) < r"
  for a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
  by (simp add: LIM_eq)

lemma LIM_offset: "f ─a→ L ⟹ (λx. f (x + k)) ─(a - k)→ L"
  for a :: "'a::real_normed_vector"
  by (simp add: filtermap_at_shift[symmetric, of a k] filterlim_def filtermap_filtermap)

lemma LIM_offset_zero: "f ─a→ L ⟹ (λh. f (a + h)) ─0→ L"
  for a :: "'a::real_normed_vector"
  by (drule LIM_offset [where k = a]) (simp add: add.commute)

lemma LIM_offset_zero_cancel: "(λh. f (a + h)) ─0→ L ⟹ f ─a→ L"
  for a :: "'a::real_normed_vector"
  by (drule LIM_offset [where k = "- a"]) simp

lemma LIM_offset_zero_iff: "NO_MATCH 0 a ⟹ f ─a→ L ⟷ (λh. f (a + h)) ─0→ L"
  for f :: "'a :: real_normed_vector ⇒ _"
  using LIM_offset_zero_cancel[of f a L] LIM_offset_zero[of f L a] by auto

lemma tendsto_offset_zero_iff:
  fixes f :: "'a :: real_normed_vector ⇒ _"
  assumes " NO_MATCH 0 a" "a ∈ S" "open S"
  shows "(f ⤏ L) (at a within S) ⟷ ((λh. f (a + h)) ⤏ L) (at 0)"
  using assms by (simp add: tendsto_within_open_NO_MATCH LIM_offset_zero_iff)

lemma LIM_zero: "(f ⤏ l) F ⟹ ((λx. f x - l) ⤏ 0) F"
  for f :: "'a ⇒ 'b::real_normed_vector"
  unfolding tendsto_iff dist_norm by simp

lemma LIM_zero_cancel:
  fixes f :: "'a ⇒ 'b::real_normed_vector"
  shows "((λx. f x - l) ⤏ 0) F ⟹ (f ⤏ l) F"
unfolding tendsto_iff dist_norm by simp

lemma LIM_zero_iff: "((λx. f x - l) ⤏ 0) F = (f ⤏ l) F"
  for f :: "'a ⇒ 'b::real_normed_vector"
  unfolding tendsto_iff dist_norm by simp

lemma LIM_imp_LIM:
  fixes f :: "'a::topological_space ⇒ 'b::real_normed_vector"
  fixes g :: "'a::topological_space ⇒ 'c::real_normed_vector"
  assumes f: "f ─a→ l"
    and le: "⋀x. x ≠ a ⟹ norm (g x - m) ≤ norm (f x - l)"
  shows "g ─a→ m"
  by (rule metric_LIM_imp_LIM [OF f]) (simp add: dist_norm le)

lemma LIM_equal2:
  fixes f g :: "'a::real_normed_vector ⇒ 'b::topological_space"
  assumes "0 < R"
    and "⋀x. x ≠ a ⟹ norm (x - a) < R ⟹ f x = g x"
  shows "g ─a→ l ⟹ f ─a→ l"
  by (rule metric_LIM_equal2 [OF _ assms]) (simp_all add: dist_norm)

lemma LIM_compose2:
  fixes a :: "'a::real_normed_vector"
  assumes f: "f ─a→ b"
    and g: "g ─b→ c"
    and inj: "∃d>0. ∀x. x ≠ a ∧ norm (x - a) < d ⟶ f x ≠ b"
  shows "(λx. g (f x)) ─a→ c"
  by (rule metric_LIM_compose2 [OF f g inj [folded dist_norm]])

lemma real_LIM_sandwich_zero:
  fixes f g :: "'a::topological_space ⇒ real"
  assumes f: "f ─a→ 0"
    and 1: "⋀x. x ≠ a ⟹ 0 ≤ g x"
    and 2: "⋀x. x ≠ a ⟹ g x ≤ f x"
  shows "g ─a→ 0"
proof (rule LIM_imp_LIM [OF f]) (* FIXME: use tendsto_sandwich *)
  fix x
  assume x: "x ≠ a"
  with 1 have "norm (g x - 0) = g x" by simp
  also have "g x ≤ f x" by (rule 2 [OF x])
  also have "f x ≤ ¦f x¦" by (rule abs_ge_self)
  also have "¦f x¦ = norm (f x - 0)" by simp
  finally show "norm (g x - 0) ≤ norm (f x - 0)" .
qed


subsection ‹Continuity›

lemma LIM_isCont_iff: "(f ─a→ f a) = ((λh. f (a + h)) ─0→ f a)"
  for f :: "'a::real_normed_vector ⇒ 'b::topological_space"
  by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel])

lemma isCont_iff: "isCont f x = (λh. f (x + h)) ─0→ f x"
  for f :: "'a::real_normed_vector ⇒ 'b::topological_space"
  by (simp add: isCont_def LIM_isCont_iff)

lemma isCont_LIM_compose2:
  fixes a :: "'a::real_normed_vector"
  assumes f [unfolded isCont_def]: "isCont f a"
    and g: "g ─f a→ l"
    and inj: "∃d>0. ∀x. x ≠ a ∧ norm (x - a) < d ⟶ f x ≠ f a"
  shows "(λx. g (f x)) ─a→ l"
  by (rule LIM_compose2 [OF f g inj])

lemma isCont_norm [simp]: "isCont f a ⟹ isCont (λx. norm (f x)) a"
  for f :: "'a::t2_space ⇒ 'b::real_normed_vector"
  by (fact continuous_norm)

lemma isCont_rabs [simp]: "isCont f a ⟹ isCont (λx. ¦f x¦) a"
  for f :: "'a::t2_space ⇒ real"
  by (fact continuous_rabs)

lemma isCont_add [simp]: "isCont f a ⟹ isCont g a ⟹ isCont (λx. f x + g x) a"
  for f :: "'a::t2_space ⇒ 'b::topological_monoid_add"
  by (fact continuous_add)

lemma isCont_minus [simp]: "isCont f a ⟹ isCont (λx. - f x) a"
  for f :: "'a::t2_space ⇒ 'b::real_normed_vector"
  by (fact continuous_minus)

lemma isCont_diff [simp]: "isCont f a ⟹ isCont g a ⟹ isCont (λx. f x - g x) a"
  for f :: "'a::t2_space ⇒ 'b::real_normed_vector"
  by (fact continuous_diff)

lemma isCont_mult [simp]: "isCont f a ⟹ isCont g a ⟹ isCont (λx. f x * g x) a"
  for f g :: "'a::t2_space ⇒ 'b::real_normed_algebra"
  by (fact continuous_mult)

lemma (in bounded_linear) isCont: "isCont g a ⟹ isCont (λx. f (g x)) a"
  by (fact continuous)

lemma (in bounded_bilinear) isCont: "isCont f a ⟹ isCont g a ⟹ isCont (λx. f x ** g x) a"
  by (fact continuous)

lemmas isCont_scaleR [simp] =
  bounded_bilinear.isCont [OF bounded_bilinear_scaleR]

lemmas isCont_of_real [simp] =
  bounded_linear.isCont [OF bounded_linear_of_real]

lemma isCont_power [simp]: "isCont f a ⟹ isCont (λx. f x ^ n) a"
  for f :: "'a::t2_space ⇒ 'b::{power,real_normed_algebra}"
  by (fact continuous_power)

lemma isCont_sum [simp]: "∀i∈A. isCont (f i) a ⟹ isCont (λx. ∑i∈A. f i x) a"
  for f :: "'a ⇒ 'b::t2_space ⇒ 'c::topological_comm_monoid_add"
  by (auto intro: continuous_sum)


subsection ‹Uniform Continuity›

lemma uniformly_continuous_on_def:
  fixes f :: "'a::metric_space ⇒ 'b::metric_space"
  shows "uniformly_continuous_on s f ⟷
    (∀e>0. ∃d>0. ∀x∈s. ∀x'∈s. dist x' x < d ⟶ dist (f x') (f x) < e)"
  unfolding uniformly_continuous_on_uniformity
    uniformity_dist filterlim_INF filterlim_principal eventually_inf_principal
  (*NEW*)
  by (force 4 3 simp: Ball_def uniformity_dist[symmetric] eventually_uniformity_metric
    where run exec: "Zip.Depth_First.all 5")
  (*ORIG*)
  (* by (force 4 3 simp: Ball_def uniformity_dist[symmetric] eventually_uniformity_metric) *)

abbreviation isUCont :: "['a::metric_space ⇒ 'b::metric_space] ⇒ bool"
  where "isUCont f ≡ uniformly_continuous_on UNIV f"

lemma isUCont_def: "isUCont f ⟷ (∀r>0. ∃s>0. ∀x y. dist x y < s ⟶ dist (f x) (f y) < r)"
  by (auto simp: uniformly_continuous_on_def dist_commute)

lemma isUCont_isCont: "isUCont f ⟹ isCont f x"
  by (drule uniformly_continuous_imp_continuous) (simp add: continuous_on_eq_continuous_at)

lemma uniformly_continuous_on_Cauchy:
  fixes f :: "'a::metric_space ⇒ 'b::metric_space"
  assumes "uniformly_continuous_on S f" "Cauchy X" "⋀n. X n ∈ S"
  shows "Cauchy (λn. f (X n))"
  using assms
  unfolding uniformly_continuous_on_def  by (meson Cauchy_def)

lemma isUCont_Cauchy: "isUCont f ⟹ Cauchy X ⟹ Cauchy (λn. f (X n))"
  by (rule uniformly_continuous_on_Cauchy[where S=UNIV and f=f]) simp_all

lemma (in bounded_linear) isUCont: "isUCont f"
  unfolding isUCont_def dist_norm
proof (intro allI impI)
  fix r :: real
  assume r: "0 < r"
  obtain K where K: "0 < K" and norm_le: "norm (f x) ≤ norm x * K" for x
    using pos_bounded by blast
  show "∃s>0. ∀x y. norm (x - y) < s ⟶ norm (f x - f y) < r"
  proof (rule exI, safe)
    from r K show "0 < r / K" by simp
  next
    fix x y :: 'a
    assume xy: "norm (x - y) < r / K"
    have "norm (f x - f y) = norm (f (x - y))" by (simp only: diff)
    also have "… ≤ norm (x - y) * K" by (rule norm_le)
    also from K xy have "… < r" by (simp only: pos_less_divide_eq)
    finally show "norm (f x - f y) < r" .
  qed
qed

lemma (in bounded_linear) Cauchy: "Cauchy X ⟹ Cauchy (λn. f (X n))"
  by (rule isUCont [THEN isUCont_Cauchy])

lemma LIM_less_bound:
  fixes f :: "real ⇒ real"
  assumes ev: "b < x" "∀ x' ∈ { b <..< x}. 0 ≤ f x'" and "isCont f x"
  shows "0 ≤ f x"
proof (rule tendsto_lowerbound)
  show "(f ⤏ f x) (at_left x)"
    using ‹isCont f x› by (simp add: filterlim_at_split isCont_def)
  show "eventually (λx. 0 ≤ f x) (at_left x)"
    using ev by (auto simp: eventually_at dist_real_def intro!: exI[of _ "x - b"])
qed simp


subsection ‹Nested Intervals and Bisection -- Needed for Compactness›

lemma nested_sequence_unique:
  assumes "∀n. f n ≤ f (Suc n)" "∀n. g (Suc n) ≤ g n" "∀n. f n ≤ g n" "(λn. f n - g n) ⇢ 0"
  shows "∃l::real. ((∀n. f n ≤ l) ∧ f ⇢ l) ∧ ((∀n. l ≤ g n) ∧ g ⇢ l)"
proof -
  have "incseq f" unfolding incseq_Suc_iff by fact
  have "decseq g" unfolding decseq_Suc_iff by fact
  have "f n ≤ g 0" for n
  proof -
    from ‹decseq g› have "g n ≤ g 0"
      by (rule decseqD) simp
    with ‹∀n. f n ≤ g n›[THEN spec, of n] show ?thesis
      by auto
  qed
  then obtain u where "f ⇢ u" "∀i. f i ≤ u"
    using incseq_convergent[OF ‹incseq f›] by auto
  moreover have "f 0 ≤ g n" for n
  proof -
    from ‹incseq f› have "f 0 ≤ f n" by (rule incseqD) simp
    with ‹∀n. f n ≤ g n›[THEN spec, of n] show ?thesis
      by simp
  qed
  then obtain l where "g ⇢ l" "∀i. l ≤ g i"
    using decseq_convergent[OF ‹decseq g›] by auto
  moreover note LIMSEQ_unique[OF assms(4) tendsto_diff[OF ‹f ⇢ u› ‹g ⇢ l›]]
  ultimately show ?thesis by auto
qed

lemma Bolzano[consumes 1, case_names trans local]:
  fixes P :: "real ⇒ real ⇒ bool"
  assumes [arith]: "a ≤ b"
    and trans: "⋀a b c. P a b ⟹ P b c ⟹ a ≤ b ⟹ b ≤ c ⟹ P a c"
    and local: "⋀x. a ≤ x ⟹ x ≤ b ⟹ ∃d>0. ∀a b. a ≤ x ∧ x ≤ b ∧ b - a < d ⟶ P a b"
  shows "P a b"
proof -
  define bisect where "bisect ≡ λ(x,y). if P x ((x+y) / 2) then ((x+y)/2, y) else (x, (x+y)/2)"
  define l u where "l n ≡ fst ((bisect^^n)(a,b))" and "u n ≡ snd ((bisect^^n)(a,b))" for n
  have l[simp]: "l 0 = a" "⋀n. l (Suc n) = (if P (l n) ((l n + u n) / 2) then (l n + u n) / 2 else l n)"
    and u[simp]: "u 0 = b" "⋀n. u (Suc n) = (if P (l n) ((l n + u n) / 2) then u n else (l n + u n) / 2)"
    by (simp_all add: l_def u_def bisect_def split: prod.split)

  have [simp]: "l n ≤ u n" for n by (induct n) auto

  have "∃x. ((∀n. l n ≤ x) ∧ l ⇢ x) ∧ ((∀n. x ≤ u n) ∧ u ⇢ x)"
  proof (safe intro!: nested_sequence_unique)
    show "l n ≤ l (Suc n)" "u (Suc n) ≤ u n" for n
      by (induct n) auto
  next
    have "l n - u n = (a - b) / 2^n" for n
      by (induct n) (auto simp: field_simps)
    then show "(λn. l n - u n) ⇢ 0"
      by (simp add: LIMSEQ_divide_realpow_zero)
  qed fact
  then obtain x where x: "⋀n. l n ≤ x" "⋀n. x ≤ u n" and "l ⇢ x" "u ⇢ x"
    by auto
  obtain d where "0 < d" and d: "a ≤ x ⟹ x ≤ b ⟹ b - a < d ⟹ P a b" for a b
    using ‹l 0 ≤ x› ‹x ≤ u 0› local[of x] by auto

  show "P a b"
  proof (rule ccontr)
    assume "¬ P a b"
    have "¬ P (l n) (u n)" for n
    proof (induct n)
      case 0
      then show ?case
        by (simp add: ‹¬ P a b›)
    next
      case (Suc n)
      with trans[of "l n" "(l n + u n) / 2" "u n"] show ?case
        by auto
    qed
    moreover
    {
      have "eventually (λn. x - d / 2 < l n) sequentially"
        using ‹0 < d› ‹l ⇢ x› by (intro order_tendstoD[of _ x]) auto
      moreover have "eventually (λn. u n < x + d / 2) sequentially"
        using ‹0 < d› ‹u ⇢ x› by (intro order_tendstoD[of _ x]) auto
      ultimately have "eventually (λn. P (l n) (u n)) sequentially"
      proof eventually_elim
        case (elim n)
        from add_strict_mono[OF this] have "u n - l n < d" by simp
        with x show "P (l n) (u n)" by (rule d)
      qed
    }
    ultimately show False by simp
  qed
qed

lemma compact_Icc[simp, intro]: "compact {a .. b::real}"
proof (cases "a ≤ b", rule compactI)
  fix C
  assume C: "a ≤ b" "∀t∈C. open t" "{a..b} ⊆ ⋃C"
  define T where "T = {a .. b}"
  from C(1,3) show "∃C'⊆C. finite C' ∧ {a..b} ⊆ ⋃C'"
  proof (induct rule: Bolzano)
    case (trans a b c)
    then have *: "{a..c} = {a..b} ∪ {b..c}"
      by auto
    with trans obtain C1 C2
      where "C1⊆C" "finite C1" "{a..b} ⊆ ⋃C1" "C2⊆C" "finite C2" "{b..c} ⊆ ⋃C2"
      by auto
    with trans show ?case
      unfolding *
        apply (intro exI[of _ "C1 ∪ C2"])
        (*NEW*)
        by (auto run exec: Zip.Breadth_First.all')
        (*ORIG*)
        (* auto *)
  next
    case (local x)
    with C have "x ∈ ⋃C" by auto
    with C(2) obtain c where "x ∈ c" "open c" "c ∈ C"
      by auto
    then obtain e where "0 < e" "{x - e <..< x + e} ⊆ c"
      by (auto simp: open_dist dist_real_def subset_eq Ball_def abs_less_iff)
    with ‹c ∈ C› show ?case
      by (safe intro!: exI[of _ "e/2"] exI[of _ "{c}"]) auto
  qed
qed simp


lemma continuous_image_closed_interval:
  fixes a b and f :: "real ⇒ real"
  defines "S ≡ {a..b}"
  assumes "a ≤ b" and f: "continuous_on S f"
  shows "∃c d. f`S = {c..d} ∧ c ≤ d"
proof -
  have S: "compact S" "S ≠ {}"
    using ‹a ≤ b› by (auto simp: S_def)
  obtain c where "c ∈ S" "∀d∈S. f d ≤ f c"
    using continuous_attains_sup[OF S f] by auto
  moreover obtain d where "d ∈ S" "∀c∈S. f d ≤ f c"
    using continuous_attains_inf[OF S f] by auto
  moreover have "connected (f`S)"
    using connected_continuous_image[OF f] connected_Icc by (auto simp: S_def)
  ultimately have "f ` S = {f d .. f c} ∧ f d ≤ f c"
    by (auto simp: connected_iff_interval)
  then show ?thesis
    by auto
qed

lemma open_Collect_positive:
  fixes f :: "'a::topological_space ⇒ real"
  assumes f: "continuous_on s f"
  shows "∃A. open A ∧ A ∩ s = {x∈s. 0 < f x}"
  using continuous_on_open_invariant[THEN iffD1, OF f, rule_format, of "{0 <..}"]
  (*NEW*)
  by (auto simp: Int_def field_simps where run exec: "Zip.Depth_First.all 1")
  (*ORIG*)
  (* by (auto simp: Int_def field_simps) *)

lemma open_Collect_less_Int:
  fixes f g :: "'a::topological_space ⇒ real"
  assumes f: "continuous_on s f"
    and g: "continuous_on s g"
  shows "∃A. open A ∧ A ∩ s = {x∈s. f x < g x}"
  using open_Collect_positive[OF continuous_on_diff[OF g f]] by (simp add: field_simps)


subsection ‹Boundedness of continuous functions›

text‹By bisection, function continuous on closed interval is bounded above›

lemma isCont_eq_Ub:
  fixes f :: "real ⇒ 'a::linorder_topology"
  shows "a ≤ b ⟹ ∀x::real. a ≤ x ∧ x ≤ b ⟶ isCont f x ⟹
    ∃M. (∀x. a ≤ x ∧ x ≤ b ⟶ f x ≤ M) ∧ (∃x. a ≤ x ∧ x ≤ b ∧ f x = M)"
  using continuous_attains_sup[of "{a..b}" f]
  (*NEW*)
  by (auto simp: continuous_at_imp_continuous_on Ball_def Bex_def
    where run exec: "Zippy.Run.Breadth_First.all'")
  (*ORIG*)
  (* by (auto simp: continuous_at_imp_continuous_on Ball_def Bex_def) *)

lemma isCont_eq_Lb:
  fixes f :: "real ⇒ 'a::linorder_topology"
  shows "a ≤ b ⟹ ∀x. a ≤ x ∧ x ≤ b ⟶ isCont f x ⟹
    ∃M. (∀x. a ≤ x ∧ x ≤ b ⟶ M ≤ f x) ∧ (∃x. a ≤ x ∧ x ≤ b ∧ f x = M)"
  using continuous_attains_inf[of "{a..b}" f]
  by (auto simp: continuous_at_imp_continuous_on Ball_def Bex_def)

lemma isCont_bounded:
  fixes f :: "real ⇒ 'a::linorder_topology"
  shows "a ≤ b ⟹ ∀x. a ≤ x ∧ x ≤ b ⟶ isCont f x ⟹ ∃M. ∀x. a ≤ x ∧ x ≤ b ⟶ f x ≤ M"
  using isCont_eq_Ub[of a b f] by auto

lemma isCont_has_Ub:
  fixes f :: "real ⇒ 'a::linorder_topology"
  shows "a ≤ b ⟹ ∀x. a ≤ x ∧ x ≤ b ⟶ isCont f x ⟹
    ∃M. (∀x. a ≤ x ∧ x ≤ b ⟶ f x ≤ M) ∧ (∀N. N < M ⟶ (∃x. a ≤ x ∧ x ≤ b ∧ N < f x))"
  using isCont_eq_Ub[of a b f] by auto

lemma isCont_Lb_Ub:
  fixes f :: "real ⇒ real"
  assumes "a ≤ b" "∀x. a ≤ x ∧ x ≤ b ⟶ isCont f x"
  shows "∃L M. (∀x. a ≤ x ∧ x ≤ b ⟶ L ≤ f x ∧ f x ≤ M) ∧
    (∀y. L ≤ y ∧ y ≤ M ⟶ (∃x. a ≤ x ∧ x ≤ b ∧ (f x = y)))"
proof -
  obtain M where M: "a ≤ M" "M ≤ b" "∀x. a ≤ x ∧ x ≤ b ⟶ f x ≤ f M"
    using isCont_eq_Ub[OF assms] by auto
  obtain L where L: "a ≤ L" "L ≤ b" "∀x. a ≤ x ∧ x ≤ b ⟶ f L ≤ f x"
    using isCont_eq_Lb[OF assms] by auto
  have "(∀x. a ≤ x ∧ x ≤ b ⟶ f L ≤ f x ∧ f x ≤ f M)"
    using M L by simp
  moreover
  have "(∀y. f L ≤ y ∧ y ≤ f M ⟶ (∃x≥a. x ≤ b ∧ f x = y))"
  proof (cases "L ≤ M")
    case True then show ?thesis
    using IVT[of f L _ M] M L assms by (metis order.trans)
  next
    case False then show ?thesis
    using IVT2[of f L _ M]
    by (metis L(2) M(1) assms(2) le_cases order.trans)
qed
  ultimately show ?thesis
    by blast
qed


text ‹Continuity of inverse function.›

lemma isCont_inverse_function:
  fixes f g :: "real ⇒ real"
  assumes d: "0 < d"
    and inj: "⋀z. ¦z-x¦ ≤ d ⟹ g (f z) = z"
    and cont: "⋀z. ¦z-x¦ ≤ d ⟹ isCont f z"
  shows "isCont g (f x)"
proof -
  let ?A = "f (x - d)"
  let ?B = "f (x + d)"
  let ?D = "{x - d..x + d}"

  have f: "continuous_on ?D f"
    using cont by (intro continuous_at_imp_continuous_on ballI) auto
  then have g: "continuous_on (f`?D) g"
    using inj by (intro continuous_on_inv) auto

  from d f have "{min ?A ?B <..< max ?A ?B} ⊆ f ` ?D"
    by (intro connected_contains_Ioo connected_continuous_image) (auto split: split_min split_max)
  with g have "continuous_on {min ?A ?B <..< max ?A ?B} g"
    by (rule continuous_on_subset)
  moreover
  have "(?A < f x ∧ f x < ?B) ∨ (?B < f x ∧ f x < ?A)"
    using d inj by (intro continuous_inj_imp_mono[OF _ _ f] inj_on_imageI2[of g, OF inj_onI]) auto
  then have "f x ∈ {min ?A ?B <..< max ?A ?B}"
    by auto
  ultimately show ?thesis
    by (simp add: continuous_on_eq_continuous_at)
qed

lemma isCont_inverse_function2:
  fixes f g :: "real ⇒ real"
  shows
    "⟦a < x; x < b;
      ⋀z. ⟦a ≤ z; z ≤ b⟧ ⟹ g (f z) = z;
      ⋀z. ⟦a ≤ z; z ≤ b⟧ ⟹ isCont f z⟧ ⟹ isCont g (f x)"
  apply (rule isCont_inverse_function [where f=f and d="min (x - a) (b - x)"])
  apply (simp_all add: abs_le_iff)
  done

text ‹Bartle/Sherbert: Introduction to Real Analysis, Theorem 4.2.9, p. 110.›
lemma LIM_fun_gt_zero: "f ─c→ l ⟹ 0 < l ⟹ ∃r. 0 < r ∧ (∀x. x ≠ c ∧ ¦c - x¦ < r ⟶ 0 < f x)"
  for f :: "real ⇒ real"
    (*NEW*)
    (*NOTE: not a minor change and hence excluded*)
    (* by (force dest: LIM_D[where r=l]) *)
    (*ORIG*)
    (*NOTE not working with zip*)
    by (force 4 4 dest: LIM_D)

lemma LIM_fun_less_zero: "f ─c→ l ⟹ l < 0 ⟹ ∃r. 0 < r ∧ (∀x. x ≠ c ∧ ¦c - x¦ < r ⟶ f x < 0)"
  for f :: "real ⇒ real"
  by (drule LIM_D [where r="-l"])
  (*NEW*)
  (force 4 4)
  (*ORIG*)
  (* (force) *)

lemma LIM_fun_not_zero: "f ─c→ l ⟹ l ≠ 0 ⟹ ∃r. 0 < r ∧ (∀x. x ≠ c ∧ ¦c - x¦ < r ⟶ f x ≠ 0)"
  for f :: "real ⇒ real"
  using LIM_fun_gt_zero[of f l c] LIM_fun_less_zero[of f l c] by (auto simp: neq_iff)

lemma Lim_topological:
  "(f ⤏ l) net ⟷
    trivial_limit net ∨ (∀S. open S ⟶ l ∈ S ⟶ eventually (λx. f x ∈ S) net)"
  unfolding tendsto_def trivial_limit_eq by auto

lemma eventually_within_Un:
  "eventually P (at x within (s ∪ t)) ⟷
    eventually P (at x within s) ∧ eventually P (at x within t)"
  unfolding eventually_at_filter
  by (auto elim!: eventually_rev_mp)

lemma Lim_within_Un:
 "(f ⤏ l) (at x within (s ∪ t)) ⟷
  (f ⤏ l) (at x within s) ∧ (f ⤏ l) (at x within t)"
  unfolding tendsto_def
  by (auto simp: eventually_within_Un)


end