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:

Technical point: in the text, the functions Unknown identifier `f`f studied are defined only on subsets Unknown identifier `X`X of ℝ : Typeℝ, and left undefined elsewhere. However, in Lean, this then creates some fiddly conversions when trying to restrict Unknown identifier `f`f to various subsets of Unknown identifier `X`X (which, technically, are not precisely subsets of ℝ : Typeℝ, 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 ℝ : Typeℝ (with the understanding that they are assigned "junk" values outside of the domain Unknown identifier `X`X of interest).

Definition 9.3.1

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

declaration uses 'sorry'example : (5:ℝ).CloseFn (.Icc 1 3) (fun x ↦ x^2) 4 := ⊢ Real.CloseFn 5 (Set.Icc 1 3) (fun x => x ^ 2) 4 All goals completed! 🐙

Example 9.3.2

declaration uses 'sorry'example : (0.41:ℝ).CloseFn (.Icc 1.9 2.1) (fun x ↦ x^2) 4 := ⊢ Real.CloseFn 0.41 (Set.Icc 1.9 2.1) (fun x => x ^ 2) 4 All goals completed! 🐙

Example 9.3.4

declaration uses 'sorry'example: ¬(0.1:ℝ).CloseFn (.Icc 1 3) (fun x ↦ x^2) 4 := ⊢ ¬Real.CloseFn 0.1 (Set.Icc 1 3) (fun x => x ^ 2) 4 All goals completed! 🐙

Example 9.3.4

declaration uses 'sorry'example: (0.1:ℝ).CloseNear (.Icc 1 3) (fun x ↦ x^2) 4 2 := ⊢ Real.CloseNear 0.1 (Set.Icc 1 3) (fun x => x ^ 2) 4 2 All goals completed! 🐙

Example 9.3.5

declaration uses 'sorry'example: ¬(0.1:ℝ).CloseFn (.Icc 1 3) (fun x ↦ x^2) 9 := ⊢ ¬Real.CloseFn 0.1 (Set.Icc 1 3) (fun x => x ^ 2) 9 All goals completed! 🐙

Example 9.3.5

declaration uses 'sorry'example: (0.1:ℝ).CloseNear (.Icc 1 3) (fun x ↦ x^2) 9 3 := ⊢ Real.CloseNear 0.1 (Set.Icc 1 3) (fun x => x ^ 2) 9 3 All 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) := X:Set ℝf:ℝ → ℝL:ℝx₀:ℝ⊢ Convergesto X f L x₀ ↔ Filter.Tendsto f (nhdsWithin x₀ X) (nhds L) X: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) 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| < ε X: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| < ε X: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| < ε X: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| < ε} X: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| < ε}X: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| < ε X: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| < ε} X: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₀+δ, X:Set ℝf:ℝ → ℝL:ℝx₀:ℝε:ℝhε:ε > 0δ:ℝleft✝:0 < δright✝:∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε⊢ x₀ - δ < x₀ ∧ x₀ < x₀ + δ All goals completed! 🐙 X: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| < ε}; X: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| < ε; All goals completed! 🐙 X: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 := X:Set ℝf:ℝ → ℝL:ℝx₀:ℝ⊢ Convergesto X f L x₀ ↔ Filter.Tendsto f (nhdsWithin x₀ X) (nhds L) All goals completed! 🐙 have h2 : 0 < u - x₀ := X:Set ℝf:ℝ → ℝL:ℝx₀:ℝ⊢ Convergesto X f L x₀ ↔ Filter.Tendsto f (nhdsWithin x₀ X) (nhds L) All goals completed! 🐙 X: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 < _fvar.2615 - _fvar.43897 := ?_mvar.44185h2:0 < _fvar.43898 - _fvar.2615 := ?_mvar.44774δ:ℝ := min (_fvar.2615 - _fvar.43897) (_fvar.43898 - _fvar.2615)⊢ ∃ δ, 0 < δ ∧ ∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε X: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 < _fvar.2615 - _fvar.43897 := ?_mvar.44185h2:0 < _fvar.43898 - _fvar.2615 := ?_mvar.44774δ:ℝ := min (_fvar.2615 - _fvar.43897) (_fvar.43898 - _fvar.2615)hδ1:min (x₀ - l) (u - x₀) ≤ x₀ - l⊢ ∃ δ, 0 < δ ∧ ∀ x ∈ X, x₀ - δ < x → x < x₀ + δ → |f x - L| < ε X: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 < _fvar.2615 - _fvar.43897 := ?_mvar.44185h2:0 < _fvar.43898 - _fvar.2615 := ?_mvar.44774δ:ℝ := min (_fvar.2615 - _fvar.43897) (_fvar.43898 - _fvar.2615)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 δ, (X: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 < _fvar.2615 - _fvar.43897 := lt_of_not_ge fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.43897) (Mathlib.Tactic.Ring.atom_pf _fvar.2615) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.2615 (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (_fvar.43897 ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add (_fvar.2615 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.2615) (Mathlib.Tactic.Ring.atom_pf _fvar.43897) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.43897 (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (_fvar.43897 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.2615 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.43897 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + (_fvar.2615 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.43897 (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.2615 (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.sub_neg_of_lt _fvar.43899) (Mathlib.Tactic.Linarith.sub_nonpos_of_le a)))h2:0 < _fvar.43898 - _fvar.2615 := lt_of_not_ge fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.2615) (Mathlib.Tactic.Ring.atom_pf _fvar.43898) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.43898 (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (_fvar.2615 ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add (_fvar.43898 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.43898) (Mathlib.Tactic.Ring.atom_pf _fvar.2615) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.2615 (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (_fvar.2615 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.43898 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.2615 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + (_fvar.43898 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.2615 (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.43898 (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.sub_neg_of_lt _fvar.43900) (Mathlib.Tactic.Linarith.sub_nonpos_of_le a)))δ:ℝ := min (_fvar.2615 - _fvar.43897) (_fvar.43898 - _fvar.2615)hδ1:min (x₀ - l) (u - x₀) ≤ x₀ - lhδ2:min (x₀ - l) (u - x₀) ≤ u - x₀⊢ 0 < δ All goals completed! 🐙); X: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 < _fvar.2615 - _fvar.43897 := ?_mvar.44185h2:0 < _fvar.43898 - _fvar.2615 := ?_mvar.44774δ:ℝ := min (_fvar.2615 - _fvar.43897) (_fvar.43898 - _fvar.2615)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 X:Set ℝf:ℝ → ℝL:ℝx₀:ℝ⊢ Convergesto X f L x₀ ↔ Filter.Tendsto f (nhdsWithin x₀ X) (nhds L) X: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 < _fvar.2615 - _fvar.43897 := lt_of_not_ge fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.43897) (Mathlib.Tactic.Ring.atom_pf _fvar.2615) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.2615 (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (_fvar.43897 ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add (_fvar.2615 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.2615) (Mathlib.Tactic.Ring.atom_pf _fvar.43897) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.43897 (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (_fvar.43897 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.2615 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.43897 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + (_fvar.2615 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.43897 (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.2615 (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.sub_neg_of_lt _fvar.43899) (Mathlib.Tactic.Linarith.sub_nonpos_of_le a)))h2:0 < _fvar.43898 - _fvar.2615 := lt_of_not_ge fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.2615) (Mathlib.Tactic.Ring.atom_pf _fvar.43898) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.43898 (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (_fvar.2615 ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add (_fvar.43898 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.43898) (Mathlib.Tactic.Ring.atom_pf _fvar.2615) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.2615 (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (_fvar.2615 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.43898 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.2615 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + (_fvar.43898 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.2615 (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.43898 (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.sub_neg_of_lt _fvar.43900) (Mathlib.Tactic.Linarith.sub_nonpos_of_le a)))δ:ℝ := min (_fvar.2615 - _fvar.43897) (_fvar.43898 - _fvar.2615)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; All goals completed! 🐙) All goals completed! 🐙

Example 9.3.8

declaration uses 'sorry'example: Convergesto (.Icc 1 3) (fun x ↦ x^2) 4 2 := ⊢ Convergesto (Set.Icc 1 3) (fun x => x ^ 2) 4 2 All goals completed! 🐙

Proposition 9.3.9 / Exercise 9.3.1

theorem declaration uses 'sorry'Convergesto.iff_conv {E:Set ℝ} (f: ℝ → ℝ) (L:ℝ) {x₀:ℝ} (h: AdherentPt x₀ E) : 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) := E:Set ℝf:ℝ → ℝL:ℝx₀:ℝh:AdherentPt x₀ E⊢ 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) All goals completed! 🐙
theorem Convergesto.comp {E:Set ℝ} {f: ℝ → ℝ} {L:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) (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) := E:Set ℝf:ℝ → ℝL:ℝx₀:ℝh:AdherentPt x₀ Ehf: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) E:Set ℝf:ℝ → ℝL:ℝx₀:ℝh:AdherentPt x₀ Ehf:∀ (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); All goals completed! 🐙
-- Remark 9.3.11 may possibly be inaccurate, in that one may be able to safely delete the hypothesis `AdherentPt x₀ E` in the above theorems. This is something that formalization might be able to clarify! If so, the hypothesis may also be deletable in several of the theorems below.

Corollary 9.3.13

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' := E: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. E: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' All goals completed! 🐙

Proposition 9.3.14 (Limit laws for functions)

theorem Convergesto.add {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) (hf: Convergesto E f L x₀) (hg: Convergesto E g M x₀) : Convergesto E (f + g) (L + M) x₀ := E:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝh:AdherentPt x₀ Ehf: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. E:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝh:AdherentPt x₀ Ehf:∀ (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)) E:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝh:AdherentPt x₀ Ehf:∀ (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)); E:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝh:AdherentPt x₀ Ehg:∀ (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)); E:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝh:AdherentPt x₀ Ea:ℕ → ℝ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)) All goals completed! 🐙

Proposition 9.3.14 (Limit laws for functions) / Exercise 9.3.2

theorem declaration uses 'sorry'Convergesto.sub {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) (hf: Convergesto E f L x₀) (hg: Convergesto E g M x₀) : Convergesto E (f - g) (L - M) x₀ := E:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝh:AdherentPt x₀ Ehf:Convergesto E f L x₀hg:Convergesto E g M x₀⊢ Convergesto E (f - g) (L - M) x₀ All goals completed! 🐙

Proposition 9.3.14 (Limit laws for functions) / Exercise 9.3.2

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

Proposition 9.3.14 (Limit laws for functions) / Exercise 9.3.2

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

Proposition 9.3.14 (Limit laws for functions) / Exercise 9.3.2

theorem declaration uses 'sorry'Convergesto.smul {E:Set ℝ} {f: ℝ → ℝ} {L:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) (hf: Convergesto E f L x₀) (c:ℝ) : Convergesto E (c • f) (c * L) x₀ := E:Set ℝf:ℝ → ℝL:ℝx₀:ℝh:AdherentPt x₀ Ehf:Convergesto E f L x₀c:ℝ⊢ Convergesto E (c • f) (c * L) x₀ All goals completed! 🐙

Proposition 9.3.14 (Limit laws for functions) / Exercise 9.3.2

theorem declaration uses 'sorry'Convergesto.mul {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) (hf: Convergesto E f L x₀) (hg: Convergesto E g M x₀) : Convergesto E (f * g) (L * M) x₀ := E:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝh:AdherentPt x₀ Ehf:Convergesto E f L x₀hg:Convergesto E g M x₀⊢ Convergesto E (f * g) (L * M) x₀ All goals completed! 🐙

Proposition 9.3.14 (Limit laws for functions) / 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₀:ℝ} (h: AdherentPt x₀ E) (hM: M ≠ 0) (hf: Convergesto E f L x₀) (hg: Convergesto E g M x₀) : Convergesto E (f / g) (L / M) x₀ := E:Set ℝf:ℝ → ℝg:ℝ → ℝL:ℝM:ℝx₀:ℝh:AdherentPt x₀ EhM:M ≠ 0hf:Convergesto E f L x₀hg:Convergesto E g M x₀⊢ Convergesto E (f / g) (L / M) x₀ All goals completed! 🐙
theorem declaration uses 'sorry'Convergesto.const {E:Set ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) (c:ℝ) : Convergesto E (fun x ↦ c) c x₀ := E:Set ℝx₀:ℝh:AdherentPt x₀ Ec:ℝ⊢ Convergesto E (fun x => c) c x₀ All goals completed! 🐙theorem declaration uses 'sorry'Convergesto.id {E:Set ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) : Convergesto E (fun x ↦ x) x₀ x₀ := E:Set ℝx₀:ℝh:AdherentPt x₀ E⊢ Convergesto E (fun x => x) x₀ x₀ All goals completed! 🐙theorem declaration uses 'sorry'Convergesto.sq {E:Set ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) : Convergesto E (fun x ↦ x^2) x₀ (x₀^2) := E:Set ℝx₀:ℝh:AdherentPt x₀ E⊢ Convergesto E (fun x => x ^ 2) x₀ (x₀ ^ 2) All goals completed! 🐙theorem declaration uses 'sorry'Convergesto.linear {E:Set ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) (c:ℝ) : Convergesto E (fun x ↦ c * x) x₀ (c * x₀) := E:Set ℝx₀:ℝh:AdherentPt x₀ Ec:ℝ⊢ Convergesto E (fun x => c * x) x₀ (c * x₀) All goals completed! 🐙theorem declaration uses 'sorry'Convergesto.quadratic {E:Set ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) (c d:ℝ) : Convergesto E (fun x ↦ x^2 + c * x + d) x₀ (x₀^2 + c * x₀ + d) := E:Set ℝx₀:ℝh:AdherentPt x₀ Ec:ℝd:ℝ⊢ Convergesto E (fun x => x ^ 2 + c * x + d) x₀ (x₀ ^ 2 + c * x₀ + d) All goals completed! 🐙theorem declaration uses 'sorry'Convergesto.restrict {X Y:Set ℝ} {f: ℝ → ℝ} {L:ℝ} {x₀:ℝ} (h: AdherentPt x₀ X) (hf: Convergesto X f L x₀) (hY: Y ⊆ X) : Convergesto Y f L x₀ := X:Set ℝY:Set ℝf:ℝ → ℝL:ℝx₀:ℝh:AdherentPt x₀ Xhf:Convergesto X f L x₀hY:Y ⊆ X⊢ Convergesto Y f L x₀ All 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

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

Example 9.3.16

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

Example 9.3.16

theorem declaration uses 'sorry'Convergesto.sign_all : ¬ ∃ L, Convergesto (.univ) Real.sign L 0 := ⊢ ¬∃ L, Convergesto Set.univ Real.sign L 0 All 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 := ⊢ Convergesto (Set.univ \ {0}) f_9_3_17 0 0 All goals completed! 🐙theorem declaration uses 'sorry'Convergesto.f_9_3_17_all : ¬ ∃ L, Convergesto .univ f_9_3_17 L 0 := ⊢ ¬∃ L, Convergesto Set.univ f_9_3_17 L 0 All goals completed! 🐙

Proposition 9.3.18 / Exercise 9.3.3

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

Example 9.3.19. The point of this example is somewhat blunted by the ability to remove the hypothesis that Unknown identifier `g`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 := ⊢ Convergesto Set.univ (fun x => (x + 2) / (x + 1)) (4 / 3) 2 All goals completed! 🐙

Example 9.3.20

declaration uses 'sorry'example : Convergesto (.univ \ {1}) (fun x ↦ (x^2-1)/(x-1)) 2 1 := ⊢ Convergesto (Set.univ \ {1}) (fun x => (x ^ 2 - 1) / (x - 1)) 2 1 All goals completed! 🐙
open Classical in /-- Example 9.3.21 -/ noncomputable abbrev f_9_3_21 : ℝ → ℝ := fun x ↦ if x ∈ (fun q:ℚ ↦ (q:ℝ)) '' .univ then 1 else 0declaration uses 'sorry'example : Filter.atTop.Tendsto (fun n ↦ f_9_3_21 (1/n:ℝ)) (nhds 1) := ⊢ Filter.Tendsto (fun n => f_9_3_21 (1 / n)) Filter.atTop (nhds 1) All goals completed! 🐙declaration uses 'sorry'example : Filter.atTop.Tendsto (fun n ↦ f_9_3_21 ((Real.sqrt 2)/n:ℝ)) (nhds 0) := ⊢ Filter.Tendsto (fun n => f_9_3_21 (√2 / n)) Filter.atTop (nhds 0) All goals completed! 🐙declaration uses 'sorry'example : ¬ ∃ L, Convergesto .univ f_9_3_21 L 0 := ⊢ ¬∃ L, Convergesto Set.univ f_9_3_21 L 0 All goals completed! 🐙
/- 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. -/

Exercise 9.3.5 (Continuous version of squeeze test)

theorem declaration uses 'sorry'Convergesto.squeeze {E:Set ℝ} {f g h: ℝ → ℝ} {L:ℝ} {x₀:ℝ} (had: AdherentPt x₀ E) (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₀ := E:Set ℝf:ℝ → ℝg:ℝ → ℝh:ℝ → ℝL:ℝx₀:ℝhad:AdherentPt x₀ Ehfg:∀ 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₀ All goals completed! 🐙
end Chapter9