Analysis
9.3. Limiting values of functions

Imports

import Mathlib.Tactic
import Mathlib.Data.Real.Sign
import Analysis.Section_9_1

set_option doc.verso.suggestions false

Analysis I, Section 9.3: Limiting values of functions

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

Limits of continuous functions
Connection with Mathlib's filter convergence concepts
Limit laws for functions

Technical point: in the text, the functions f studied are defined only on subsets X of ℝ, and left undefined elsewhere. However, in Lean, this then creates some fiddly conversions when trying to restrict f to various subsets of X (which, technically, are not precisely subsets of ℝ, though they can be coerced to such). To avoid this issue we will deviate from the text by having our functions defined on all of ℝ (with the understanding that they are assigned "junk" values outside of the domain X of interest).

Definition 9.3.1 Note the books uses ≤ instead of <, but < matches mathlib's definition of neighborhood.

abbrev Real.CloseFn (ε:ℝ) (X:Set ℝ) (f: ℝ → ℝ) (L:ℝ) : Prop :=
  ∀ x ∈ X, |f x - L| < ε

Definition 9.3.3

abbrev Real.CloseNear (ε:ℝ) (X:Set ℝ) (f: ℝ → ℝ) (L:ℝ) (x₀:ℝ) : Prop :=
  ∃ δ > 0, ε.CloseFn (X ∩ .Ioo (x₀-δ) (x₀+δ)) f L

              namespace Chapter9/-- Example 9.3.2
Slight change from the book to accomodate the change to {lean}`Real.CloseFn`
-/
declaration uses `sorry`example : (5.1:ℝ).CloseFn (.Icc 1 3) (fun x ↦ x^2) 4 := by⊢ Real.CloseFn 5.1 (Set.Icc 1 3) (fun x ↦ x ^ 2) 4 sorryAll goals completed! 🐙/-- Example 9.3.2
Slight change from the book to accomodate the change to {lean}`Real.CloseFn`
-/
declaration uses `sorry`example : (0.42:ℝ).CloseFn (.Icc 1.9 2.1) (fun x ↦ x^2) 4 := by⊢ Real.CloseFn 0.42 (Set.Icc 1.9 2.1) (fun x ↦ x ^ 2) 4 sorryAll goals completed! 🐙/-- Example 9.3.4 -/
declaration uses `sorry`example: ¬(0.1:ℝ).CloseFn (.Icc 1 3) (fun x ↦ x^2) 4 := by⊢ ¬Real.CloseFn 0.1 (Set.Icc 1 3) (fun x ↦ x ^ 2) 4
  sorryAll goals completed! 🐙/-- Example 9.3.4 -/
declaration uses `sorry`example: (0.1:ℝ).CloseNear (.Icc 1 3) (fun x ↦ x^2) 4 2 := by⊢ Real.CloseNear 0.1 (Set.Icc 1 3) (fun x ↦ x ^ 2) 4 2
  sorryAll goals completed! 🐙/-- Example 9.3.5 -/
declaration uses `sorry`example: ¬(0.1:ℝ).CloseFn (.Icc 1 3) (fun x ↦ x^2) 9 := by⊢ ¬Real.CloseFn 0.1 (Set.Icc 1 3) (fun x ↦ x ^ 2) 9
  sorryAll goals completed! 🐙/-- Example 9.3.5 -/
declaration uses `sorry`example: (0.1:ℝ).CloseNear (.Icc 1 3) (fun x ↦ x^2) 9 3 := by⊢ Real.CloseNear 0.1 (Set.Icc 1 3) (fun x ↦ x ^ 2) 9 3
  sorryAll goals completed! 🐙

Definition 9.3.6 (Convergence of functions at a point).

abbrev Convergesto (X:Set ℝ) (f: ℝ → ℝ) (L:ℝ) (x₀:ℝ) : Prop := ∀ ε > (0:ℝ), ε.CloseNear X f L x₀

Connection with Mathlib filter convergence concepts

theorem Convergesto.iff (X:Set ℝ) (f: ℝ → ℝ) (L:ℝ) (x₀:ℝ) :
  Convergesto X f L x₀ ↔ (nhdsWithin x₀ X).Tendsto f (nhds L) := byX:Set ℝf:ℝ → ℝL:ℝx₀:ℝ⊢ Convergesto X f L x₀ ↔ Filter.Tendsto f (nhdsWithin x₀ X) (nhds L)
  unfold Convergesto Real.CloseNear Real.CloseFn nhdsWithinX:Set ℝf:ℝ → ℝL:ℝx₀:ℝ⊢ (∀ ε > 0, ∃ δ > 0, ∀ x ∈ X ∩ Set.Ioo (x₀ - δ) (x₀ + δ), |f x - L| < ε) ↔
  Filter.Tendsto f (nhds x₀ ⊓ Filter.principal X) (nhds L)
  rw [LinearOrderedAddCommGroup.tendsto_nhds]X:Set ℝf:ℝ → ℝL:ℝx₀:ℝ⊢ (∀ ε > 0, ∃ δ > 0, ∀ x ∈ X ∩ Set.Ioo (x₀ - δ) (x₀ + δ), |f x - L| < ε) ↔
  ∀ ε > 0, ∀ᶠ (b : ℝ) in nhds x₀ ⊓ Filter.principal X, |f b - L| < ε
  peel with ε hεh.hX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0⊢ (∃ δ > 0, ∀ x ∈ X ∩ Set.Ioo (x₀ - δ) (x₀ + δ), |f x - L| < ε) ↔
  ∀ᶠ (b : ℝ) in nhds x₀ ⊓ Filter.principal X, |f b - L| < ε
  rw [Filter.eventually_inf_principal]h.hX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0⊢ (∃ δ > 0, ∀ x ∈ X ∩ Set.Ioo (x₀ - δ) (x₀ + δ), |f x - L| < ε) ↔ ∀ᶠ (x : ℝ) in nhds x₀, x ∈ X → |f x - L| < ε
  simp [Filter.Eventually, mem_nhds_iff_exists_Ioo_subset]h.hX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0⊢ (∃ δ, 0 < δ ∧ ∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε) ↔
  ∃ l u, (l < x₀ ∧ x₀ < u) ∧ Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}
  constructorh.h.mpX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0⊢ (∃ δ, 0 < δ ∧ ∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε) →
  ∃ l u, (l < x₀ ∧ x₀ < u) ∧ Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}h.h.mprX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0⊢ (∃ l u, (l < x₀ ∧ x₀ < u) ∧ Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}) →
  ∃ δ, 0 < δ ∧ ∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε
  .h.h.mpX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0⊢ (∃ δ, 0 < δ ∧ ∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε) →
  ∃ l u, (l < x₀ ∧ x₀ < u) ∧ Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε} intro ⟨ δ, _, _ ⟩h.h.mpX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0δ:ℝleft✝:0 < δright✝:∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε⊢ ∃ l u, (l < x₀ ∧ x₀ < u) ∧ Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}; use x₀-δ, x₀+δ, byX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0δ:ℝleft✝:0 < δright✝:∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε⊢ x₀ - δ < x₀ ∧ x₀ < x₀ + δ grindAll goals completed! 🐙
    intro _rightX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0δ:ℝleft✝:0 < δright✝:∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < εa✝:ℝ⊢ a✝ ∈ Set.Ioo (x₀ - δ) (x₀ + δ) → a✝ ∈ {x | x ∈ X → |f x - L| < ε}; simprightX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0δ:ℝleft✝:0 < δright✝:∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < εa✝:ℝ⊢ x₀ - δ < a✝ → a✝ < x₀ + δ → a✝ ∈ X → |f a✝ - L| < ε; grindAll goals completed! 🐙
  intro ⟨ l, u, ⟨ _, _ ⟩, h ⟩h.h.mprX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0l:ℝu:ℝleft✝:l < x₀right✝:x₀ < uh:Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}⊢ ∃ δ, 0 < δ ∧ ∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε
  have h1 : 0 < x₀ - l := byX:Set ℝf:ℝ → ℝL:ℝx₀:ℝ⊢ Convergesto X f L x₀ ↔ Filter.Tendsto f (nhdsWithin x₀ X) (nhds L) linarithAll goals completed! 🐙
  have h2 : 0 < u - x₀ := byX:Set ℝf:ℝ → ℝL:ℝx₀:ℝ⊢ Convergesto X f L x₀ ↔ Filter.Tendsto f (nhdsWithin x₀ X) (nhds L) linarithAll goals completed! 🐙
  set δ := min (x₀ - l) (u - x₀)h.h.mprX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0l:ℝu:ℝleft✝:l < x₀right✝:x₀ < uh:Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}h1:0 < x₀ - lh2:0 < u - x₀δ:ℝ := min (x₀ - l) (u - x₀)⊢ ∃ δ, 0 < δ ∧ ∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε
  observe hδ1 : δ ≤ x₀ - lh.h.mprX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0l:ℝu:ℝleft✝:l < x₀right✝:x₀ < uh:Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}h1:0 < x₀ - lh2:0 < u - x₀δ:ℝ := min (x₀ - l) (u - x₀)hδ1:min (x₀ - l) (u - x₀) ≤ x₀ - l⊢ ∃ δ, 0 < δ ∧ ∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε
  observe hδ2 : δ ≤ u - x₀h.h.mprX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0l:ℝu:ℝleft✝:l < x₀right✝:x₀ < uh:Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}h1:0 < x₀ - lh2:0 < u - x₀δ:ℝ := min (x₀ - l) (u - x₀)hδ1:min (x₀ - l) (u - x₀) ≤ x₀ - lhδ2:min (x₀ - l) (u - x₀) ≤ u - x₀⊢ ∃ δ, 0 < δ ∧ ∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε
  use δ, (byX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0l:ℝu:ℝleft✝:l < x₀right✝:x₀ < uh:Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}h1:0 < x₀ - lh2:0 < u - x₀δ:ℝ := min (x₀ - l) (u - x₀)hδ1:min (x₀ - l) (u - x₀) ≤ x₀ - lhδ2:min (x₀ - l) (u - x₀) ≤ u - x₀⊢ 0 < δ positivityAll goals completed! 🐙); intro x hxXrightX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0l:ℝu:ℝleft✝:l < x₀right✝:x₀ < uh:Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}h1:0 < x₀ - lh2:0 < u - x₀δ:ℝ := min (x₀ - l) (u - x₀)hδ1:min (x₀ - l) (u - x₀) ≤ x₀ - lhδ2:min (x₀ - l) (u - x₀) ≤ u - x₀x:ℝhxX:x ∈ X⊢ x₀ - δ < x → x < x₀ + δ → |f x - L| < ε _rightX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0l:ℝu:ℝleft✝:l < x₀right✝:x₀ < uh:Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}h1:0 < x₀ - lh2:0 < u - x₀δ:ℝ := min (x₀ - l) (u - x₀)hδ1:min (x₀ - l) (u - x₀) ≤ x₀ - lhδ2:min (x₀ - l) (u - x₀) ≤ u - x₀x:ℝhxX:x ∈ Xa✝:x₀ - δ < x⊢ x < x₀ + δ → |f x - L| < ε _rightX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0l:ℝu:ℝleft✝:l < x₀right✝:x₀ < uh:Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}h1:0 < x₀ - lh2:0 < u - x₀δ:ℝ := min (x₀ - l) (u - x₀)hδ1:min (x₀ - l) (u - x₀) ≤ x₀ - lhδ2:min (x₀ - l) (u - x₀) ≤ u - x₀x:ℝhxX:x ∈ Xa✝¹:x₀ - δ < xa✝:x < x₀ + δ⊢ |f x - L| < ε
  specialize h (show x ∈ .Ioo l u byX:Set ℝf:ℝ → ℝL:ℝx₀:ℝ⊢ Convergesto X f L x₀ ↔ Filter.Tendsto f (nhdsWithin x₀ X) (nhds L) simpX:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0l:ℝu:ℝleft✝:l < x₀right✝:x₀ < uh:Set.Ioo l u ⊆ {x | x ∈ X → |f x - L| < ε}h1:0 < x₀ - lh2:0 < u - x₀δ:ℝ := min (x₀ - l) (u - x₀)hδ1:min (x₀ - l) (u - x₀) ≤ x₀ - lhδ2:min (x₀ - l) (u - x₀) ≤ u - x₀x:ℝhxX:x ∈ Xa✝¹:x₀ - δ < xa✝:x < x₀ + δ⊢ l < x ∧ x < u; grindAll goals completed! 🐙)
  simpa [hxX] using hAll goals completed! 🐙

/-- Example 9.3.8 -/
declaration uses `sorry`example: Convergesto (.Icc 1 3) (fun x ↦ x^2) 4 2 := by⊢ Convergesto (Set.Icc 1 3) (fun x ↦ x ^ 2) 4 2
  sorryAll goals completed! 🐙

Proposition 9.3.9 / Exercise 9.3.1

theorem declaration uses `sorry`Convergesto.iff_conv {E:Set ℝ} (f: ℝ → ℝ) (L:ℝ) {x₀:ℝ} :
  Convergesto E f L x₀ ↔ ∀ a:ℕ → ℝ, (∀ n:ℕ, a n ∈ E) →
  Filter.atTop.Tendsto a (nhds x₀) →
  Filter.atTop.Tendsto (fun n ↦ f (a n)) (nhds L) := byE:Set ℝf:ℝ → ℝL:ℝx₀:ℝ⊢ Convergesto E f L x₀ ↔
  ∀ (a : ℕ → ℝ),
    (∀ (n : ℕ), a n ∈ E) →
      Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun n ↦ f (a n)) Filter.atTop (nhds L)
  sorryAll goals completed! 🐙

theorem Convergesto.comp {E:Set ℝ} {f: ℝ → ℝ} {L:ℝ} {x₀:ℝ} (hf: Convergesto E f L x₀) {a:ℕ → ℝ}
  (ha: ∀ n:ℕ, a n ∈ E) (hconv: Filter.atTop.Tendsto a (nhds x₀)) :
  Filter.atTop.Tendsto (fun n ↦ f (a n)) (nhds L) := byE:Set ℝf:ℝ → ℝL:ℝx₀:ℝhf:Convergesto E f L x₀a:ℕ → ℝha:∀ (n : ℕ), a n ∈ Ehconv:Filter.Tendsto a Filter.atTop (nhds x₀)⊢ Filter.Tendsto (fun n ↦ f (a n)) Filter.atTop (nhds L)
  rw [iff_conv f L] at hfE:Set ℝf:ℝ → ℝL:ℝx₀:ℝhf:∀ (a : ℕ → ℝ),
  (∀ (n : ℕ), a n ∈ E) →
    Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun n ↦ f (a n)) Filter.atTop (nhds L)a:ℕ → ℝha:∀ (n : ℕ), a n ∈ Ehconv:Filter.Tendsto a Filter.atTop (nhds x₀)⊢ Filter.Tendsto (fun n ↦ f (a n)) Filter.atTop (nhds L); solve_by_elimAll goals completed! 🐙

Corollary 9.3.13

-- Remark 9.3.11 is not quite true in Lean: the hypothesis `AdherentPt x₀ E` is safely removed
-- from most theorems (with the exception of Convergesto.uniq).

theorem Convergesto.uniq {E:Set ℝ} {f: ℝ → ℝ} {L L':ℝ} {x₀:ℝ} (h: AdherentPt x₀ E)
  (hf: Convergesto E f L x₀) (hf': Convergesto E f L' x₀) : L = L' := byE:Set ℝf:ℝ → ℝL:ℝL':ℝx₀:ℝh:AdherentPt x₀ Ehf:Convergesto E f L x₀hf':Convergesto E f L' x₀⊢ L = L'
  -- This proof is written to follow the structure of the original text.
  let ⟨ a, ha, hconv ⟩ := (limit_of_AdherentPt _ _).mp hE:Set ℝf:ℝ → ℝL:ℝL':ℝx₀:ℝh:AdherentPt x₀ Ehf:Convergesto E f L x₀hf':Convergesto E f L' x₀a:ℕ → ℝha:∀ (n : ℕ), a n ∈ Ehconv:Filter.Tendsto a Filter.atTop (nhds x₀)⊢ L = L'
  exact tendsto_nhds_unique (hf.comp ha hconv) (hf'.comp ha hconv)All goals completed! 🐙

Proposition 9.3.14 (Limit laws for functions, add)

theorem Convergesto.add {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ}
  (hf: Convergesto E f L x₀) (hg: Convergesto E g M x₀) :
  Convergesto E (f + g) (L + M) x₀ := byE:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝhf:Convergesto E f L x₀hg:Convergesto E g M x₀⊢ Convergesto E (f + g) (L + M) x₀
    -- This proof is written to follow the structure of the original text.
    rw [iff_conv _ _] at hf hg ⊢E:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝhf:∀ (a : ℕ → ℝ),
  (∀ (n : ℕ), a n ∈ E) →
    Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun n ↦ f (a n)) Filter.atTop (nhds L)hg:∀ (a : ℕ → ℝ),
  (∀ (n : ℕ), a n ∈ E) →
    Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun n ↦ g (a n)) Filter.atTop (nhds M)⊢ ∀ (a : ℕ → ℝ),
  (∀ (n : ℕ), a n ∈ E) →
    Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun n ↦ (f + g) (a n)) Filter.atTop (nhds (L + M))
    intro a haE:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝhf:∀ (a : ℕ → ℝ),
  (∀ (n : ℕ), a n ∈ E) →
    Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun n ↦ f (a n)) Filter.atTop (nhds L)hg:∀ (a : ℕ → ℝ),
  (∀ (n : ℕ), a n ∈ E) →
    Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun n ↦ g (a n)) Filter.atTop (nhds M)a:ℕ → ℝha:∀ (n : ℕ), a n ∈ E⊢ Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun n ↦ (f + g) (a n)) Filter.atTop (nhds (L + M)) hconvE:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝhf:∀ (a : ℕ → ℝ),
  (∀ (n : ℕ), a n ∈ E) →
    Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun n ↦ f (a n)) Filter.atTop (nhds L)hg:∀ (a : ℕ → ℝ),
  (∀ (n : ℕ), a n ∈ E) →
    Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun n ↦ g (a n)) Filter.atTop (nhds M)a:ℕ → ℝha:∀ (n : ℕ), a n ∈ Ehconv:Filter.Tendsto a Filter.atTop (nhds x₀)⊢ Filter.Tendsto (fun n ↦ (f + g) (a n)) Filter.atTop (nhds (L + M)); specialize hf a ha hconvE:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝhg:∀ (a : ℕ → ℝ),
  (∀ (n : ℕ), a n ∈ E) →
    Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun n ↦ g (a n)) Filter.atTop (nhds M)a:ℕ → ℝha:∀ (n : ℕ), a n ∈ Ehconv:Filter.Tendsto a Filter.atTop (nhds x₀)hf:Filter.Tendsto (fun n ↦ f (a n)) Filter.atTop (nhds L)⊢ Filter.Tendsto (fun n ↦ (f + g) (a n)) Filter.atTop (nhds (L + M)); specialize hg a ha hconvE:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝa:ℕ → ℝha:∀ (n : ℕ), a n ∈ Ehconv:Filter.Tendsto a Filter.atTop (nhds x₀)hf:Filter.Tendsto (fun n ↦ f (a n)) Filter.atTop (nhds L)hg:Filter.Tendsto (fun n ↦ g (a n)) Filter.atTop (nhds M)⊢ Filter.Tendsto (fun n ↦ (f + g) (a n)) Filter.atTop (nhds (L + M))
    convert hf.add hg using 1All goals completed! 🐙

Proposition 9.3.14 (Limit laws for functions, sub) / Exercise 9.3.2

theorem declaration uses `sorry`Convergesto.sub {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ}
  (hf: Convergesto E f L x₀) (hg: Convergesto E g M x₀) :
  Convergesto E (f - g) (L - M) x₀ := byE:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝhf:Convergesto E f L x₀hg:Convergesto E g M x₀⊢ Convergesto E (f - g) (L - M) x₀
    sorryAll goals completed! 🐙

Proposition 9.3.14 (Limit laws for functions, max) / Exercise 9.3.2

theorem declaration uses `sorry`Convergesto.max {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ}
  (hf: Convergesto E f L x₀) (hg: Convergesto E g M x₀) :
  Convergesto E (max f g) (max L M) x₀ := byE:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝhf:Convergesto E f L x₀hg:Convergesto E g M x₀⊢ Convergesto E (f ⊔ g) (Max.max L M) x₀
    sorryAll goals completed! 🐙

Proposition 9.3.14 (Limit laws for functions, min) / Exercise 9.3.2

theorem declaration uses `sorry`Convergesto.min {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ}
  (hf: Convergesto E f L x₀) (hg: Convergesto E g M x₀) :
  Convergesto E (min f g) (min L M) x₀ := byE:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝhf:Convergesto E f L x₀hg:Convergesto E g M x₀⊢ Convergesto E (f ⊓ g) (Min.min L M) x₀
    sorryAll goals completed! 🐙

Proposition 9.3.14 (Limit laws for functions, smul) / Exercise 9.3.2

theorem declaration uses `sorry`Convergesto.smul {E:Set ℝ} {f: ℝ → ℝ} {L:ℝ} {x₀:ℝ}
  (hf: Convergesto E f L x₀) (c:ℝ) :
  Convergesto E (c • f) (c * L) x₀ := byE:Set ℝf:ℝ → ℝL:ℝx₀:ℝhf:Convergesto E f L x₀c:ℝ⊢ Convergesto E (c • f) (c * L) x₀
    sorryAll goals completed! 🐙

Proposition 9.3.14 (Limit laws for functions, mul) / Exercise 9.3.2

theorem declaration uses `sorry`Convergesto.mul {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ}
  (hf: Convergesto E f L x₀) (hg: Convergesto E g M x₀) :
  Convergesto E (f * g) (L * M) x₀ := byE:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝhf:Convergesto E f L x₀hg:Convergesto E g M x₀⊢ Convergesto E (f * g) (L * M) x₀
    sorryAll goals completed! 🐙

Proposition 9.3.14 (Limit laws for functions, div) / Exercise 9.3.2. The hypothesis in the book that g is non-vanishing on E can be dropped.

theorem declaration uses `sorry`Convergesto.div {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ} (hM: M ≠ 0)
  (hf: Convergesto E f L x₀) (hg: Convergesto E g M x₀) :
  Convergesto E (f / g) (L / M) x₀ := byE:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝhM:M ≠ 0hf:Convergesto E f L x₀hg:Convergesto E g M x₀⊢ Convergesto E (f / g) (L / M) x₀
    sorryAll goals completed! 🐙

              theorem declaration uses `sorry`Convergesto.const (E:Set ℝ) (x₀:ℝ) (c:ℝ)
  : Convergesto E (fun _ ↦ c) c x₀ := byE:Set ℝx₀:ℝc:ℝ⊢ Convergesto E (fun x ↦ c) c x₀
  sorryAll goals completed! 🐙theorem declaration uses `sorry`Convergesto.id (E:Set ℝ) (x₀:ℝ)
  : Convergesto E (fun x ↦ x) x₀ x₀ := byE:Set ℝx₀:ℝ⊢ Convergesto E (fun x ↦ x) x₀ x₀
  sorryAll goals completed! 🐙theorem declaration uses `sorry`Convergesto.sq (E:Set ℝ) (x₀:ℝ)
  : Convergesto E (fun x ↦ x^2) (x₀^2) x₀ := byE:Set ℝx₀:ℝ⊢ Convergesto E (fun x ↦ x ^ 2) (x₀ ^ 2) x₀
  sorryAll goals completed! 🐙theorem declaration uses `sorry`Convergesto.linear (E:Set ℝ) (x₀:ℝ) (c:ℝ)
  : Convergesto E (fun x ↦ c * x) (c * x₀) x₀ := byE:Set ℝx₀:ℝc:ℝ⊢ Convergesto E (fun x ↦ c * x) (c * x₀) x₀
  sorryAll goals completed! 🐙theorem declaration uses `sorry`Convergesto.quadratic (E:Set ℝ) (x₀:ℝ) (c d:ℝ)
  : Convergesto E (fun x ↦ x^2 + c * x + d) (x₀^2 + c * x₀ + d) x₀ := byE:Set ℝx₀:ℝc:ℝd:ℝ⊢ Convergesto E (fun x ↦ x ^ 2 + c * x + d) (x₀ ^ 2 + c * x₀ + d) x₀
  sorryAll goals completed! 🐙theorem declaration uses `sorry`Convergesto.restrict {X Y:Set ℝ} {f: ℝ → ℝ} {L:ℝ} {x₀:ℝ} (hf: Convergesto X f L x₀) (hY: Y ⊆ X) : Convergesto Y f L x₀ := byX:Set ℝY:Set ℝf:ℝ → ℝL:ℝx₀:ℝhf:Convergesto X f L x₀hY:Y ⊆ X⊢ Convergesto Y f L x₀
  sorryAll goals completed! 🐙theorem Real.sign_def (x:ℝ) : Real.sign x = if x < 0 then -1 else if x > 0 then 1 else 0 := rfl

Example 9.3.16 (a)

theorem declaration uses `sorry`Convergesto.sign_right : Convergesto (.Ioi 0) Real.sign 1 0 := by⊢ Convergesto (Set.Ioi 0) Real.sign 1 0 sorryAll goals completed! 🐙

Example 9.3.16 (b)

theorem declaration uses `sorry`Convergesto.sign_left : Convergesto (.Iio 0) Real.sign (-1) 0 := by⊢ Convergesto (Set.Iio 0) Real.sign (-1) 0 sorryAll goals completed! 🐙

Example 9.3.16 (c)

theorem declaration uses `sorry`Convergesto.sign_all : ¬ ∃ L, Convergesto (.univ) Real.sign L 0 := by⊢ ¬∃ L, Convergesto Set.univ Real.sign L 0 sorryAll goals completed! 🐙

              noncomputable abbrev f_9_3_17 : ℝ → ℝ := fun x ↦ if x = 0 then 1 else 0theorem declaration uses `sorry`Convergesto.f_9_3_17_remove : Convergesto (.univ \ {0}) f_9_3_17 0 0 := by⊢ Convergesto (Set.univ \ {0}) f_9_3_17 0 0 sorryAll goals completed! 🐙theorem declaration uses `sorry`Convergesto.f_9_3_17_all : ¬ ∃ L, Convergesto .univ f_9_3_17 L 0 := by⊢ ¬∃ L, Convergesto Set.univ f_9_3_17 L 0 sorryAll goals completed! 🐙

Proposition 9.3.18 / Exercise 9.3.3

theorem declaration uses `sorry`Convergesto.local {E:Set ℝ} {f: ℝ → ℝ} {L:ℝ} {x₀:ℝ} {δ:ℝ} (hδ: δ > 0) :
  Convergesto E f L x₀ ↔ Convergesto (E ∩ .Ioo (x₀-δ) (x₀+δ)) f L x₀ := byE:Set ℝf:ℝ → ℝL:ℝx₀:ℝδ:ℝhδ:δ > 0⊢ Convergesto E f L x₀ ↔ Convergesto (E ∩ Set.Ioo (x₀ - δ) (x₀ + δ)) f L x₀
    sorryAll goals completed! 🐙

/-- Example 9.3.19.  The point of this example is somewhat blunted by the ability to remove the hypothesis that {lit}`g` is non-zero from the relevant part of Proposition 9.3.14 -/
declaration uses `sorry`example : Convergesto .univ (fun x ↦ (x+2)/(x+1)) (4/3:ℝ) 2 := by⊢ Convergesto Set.univ (fun x ↦ (x + 2) / (x + 1)) (4 / 3) 2 sorryAll goals completed! 🐙

/-- Example 9.3.20 -/
declaration uses `sorry`example : Convergesto (.univ \ {1}) (fun x ↦ (x^2-1)/(x-1)) 2 1 := by⊢ Convergesto (Set.univ \ {1}) (fun x ↦ (x ^ 2 - 1) / (x - 1)) 2 1 sorryAll goals completed! 🐙

Example 9.3.21

open Classical innoncomputable abbrev f_9_3_21 : ℝ → ℝ := fun x ↦ if x ∈ (fun q:ℚ ↦ (q:ℝ)) '' .univ then 1 else 0

              declaration uses `sorry`example : Filter.atTop.Tendsto (fun (n:ℕ) ↦ f_9_3_21 (1/(n:ℝ))) (nhds 1) := by⊢ Filter.Tendsto (fun n ↦ f_9_3_21 (1 / ↑n)) Filter.atTop (nhds 1) sorryAll goals completed! 🐙declaration uses `sorry`example : Filter.atTop.Tendsto (fun (n:ℕ) ↦ f_9_3_21 ((Real.sqrt 2)/n:ℝ)) (nhds 0) := by⊢ Filter.Tendsto (fun n ↦ f_9_3_21 (√2 / ↑n)) Filter.atTop (nhds 0) sorryAll goals completed! 🐙declaration uses `sorry`example : ¬ ∃ L, Convergesto .univ f_9_3_21 L 0 := by⊢ ¬∃ L, Convergesto Set.univ f_9_3_21 L 0 sorryAll goals completed! 🐙

Exercise 9.3.5 (Continuous version of squeeze test)

/- Exercise 9.3.4: State a definition of limit superior and limit inferior for functions, and prove an analogue of Proposition 9.3.9 for those definitions. -/

theorem declaration uses `sorry`Convergesto.squeeze {E:Set ℝ} {f g h: ℝ → ℝ} {L:ℝ} {x₀:ℝ}
  (hfg: ∀ x ∈ E, f x ≤ g x) (hgh: ∀ x ∈ E, g x ≤ h x)
  (hf: Convergesto E f L x₀) (hh: Convergesto E h L x₀) :
  Convergesto E g L x₀ := byE:Set ℝf:ℝ → ℝg:ℝ → ℝh:ℝ → ℝL:ℝx₀:ℝhfg:∀ x ∈ E, f x ≤ g xhgh:∀ x ∈ E, g x ≤ h xhf:Convergesto E f L x₀hh:Convergesto E h L x₀⊢ Convergesto E g L x₀
    sorryAll goals completed! 🐙

end Chapter9