From 76cf7ab1c08fae7153d257e34a968bd5e41fe9ae Mon Sep 17 00:00:00 2001 From: Rado Kirov Date: Fri, 10 Apr 2026 20:58:53 -0700 Subject: [PATCH] Section 9.3: remove unnecessary AdherentPt hypotheses and fix statements MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Remark 9.3.11 asked whether the AdherentPt hypothesis could be removed from Proposition 9.3.9 and subsequent theorems. Formalization confirms it can. This removes AdherentPt from 17 theorem statements (keeping it only in Convergesto.uniq where it is genuinely needed). Other statement fixes: - Example 9.3.2 constants: 5 → 5.1, 0.41 → 0.42 (needed for strict <) - sq, linear, quadratic: fix argument order (limit before point) - const, id, sq, linear, quadratic: implicit → explicit args - const body: fun x ↦ c → fun _ ↦ c Co-Authored-By: Claude Opus 4.6 (1M context) --- Analysis/Section_10_4.lean | 12 ++----- Analysis/Section_10_5.lean | 1 - Analysis/Section_9_3.lean | 68 +++++++++++++++++++++----------------- Analysis/Section_9_4.lean | 12 +++---- Analysis/Section_9_5.lean | 4 +-- Analysis/Section_9_6.lean | 2 +- 6 files changed, 49 insertions(+), 50 deletions(-) diff --git a/Analysis/Section_10_4.lean b/Analysis/Section_10_4.lean index 5d7c6129..a7d5f491 100644 --- a/Analysis/Section_10_4.lean +++ b/Analysis/Section_10_4.lean @@ -61,14 +61,7 @@ theorem inverse_function_theorem {X Y: Set ℝ} {f: ℝ → ℝ} {g:ℝ → ℝ} (hf: HasDerivWithinAt f f'x₀ X x₀) (hg: ContinuousWithinAt g Y y₀) : HasDerivWithinAt g (1/f'x₀) Y y₀ := by -- This proof is written to follow the structure of the original text. - have had : AdherentPt y₀ (Y \ {y₀}) := by - simp [←AdherentPt_def, limit_of_AdherentPt] at * - choose x hx hconv using hcluster; use f ∘ x - split_ands; grind - rw [←hfx₀] - apply hconv.comp_of_continuous hx₀ _ (fun n ↦ (hx n).1) - exact ContinuousWithinAt.of_differentiableWithinAt (DifferentiableWithinAt.of_hasDeriv hf) - rw [HasDerivWithinAt.iff, ←Convergesto.iff, Convergesto.iff_conv _ _ had] + rw [HasDerivWithinAt.iff, ←Convergesto.iff, Convergesto.iff_conv _ _] intro y hy hconv set x : ℕ → ℝ := fun n ↦ g (y n) have hy' : ∀ n, y n ∈ Y := by aesop @@ -76,9 +69,8 @@ theorem inverse_function_theorem {X Y: Set ℝ} {f: ℝ → ℝ} {g:ℝ → ℝ} have hx : ∀ n, x n ∈ X \ {x₀}:= by sorry replace hconv := hconv.comp_of_continuous hy₀ hg hy' - have had' : AdherentPt x₀ (X \ {x₀}) := by rwa [AdherentPt_def] have hgy₀ : g y₀ = x₀ := by aesop - rw [HasDerivWithinAt.iff, ←Convergesto.iff, Convergesto.iff_conv _ _ had'] at hf + rw [HasDerivWithinAt.iff, ←Convergesto.iff, Convergesto.iff_conv _ _] at hf convert (hf _ hx _).inv₀ _ using 2 with n <;> grind /-- Exercise 10.4.1(a) -/ diff --git a/Analysis/Section_10_5.lean b/Analysis/Section_10_5.lean index 9e772ea7..d5b2402b 100644 --- a/Analysis/Section_10_5.lean +++ b/Analysis/Section_10_5.lean @@ -93,7 +93,6 @@ theorem _root_.Filter.Tendsto.of_div' {a b L:ℝ} (hab: a < b) {f g f' g': ℝ simp_rw [hy']; apply hderiv.comp solve_by_elim [tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within, Filter.Eventually.of_forall] - simp [←closure_def', closure_Ioc (show a ≠ b by grind)]; grind end Chapter10 diff --git a/Analysis/Section_9_3.lean b/Analysis/Section_9_3.lean index 41160917..04720ecc 100644 --- a/Analysis/Section_9_3.lean +++ b/Analysis/Section_9_3.lean @@ -27,7 +27,9 @@ our functions defined on all of {lean}`ℝ` (with the understanding that they ar outside of the domain `X` of interest). -/ -/-- Definition 9.3.1 -/ +/-- 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| < ε @@ -37,11 +39,15 @@ abbrev Real.CloseNear (ε:ℝ) (X:Set ℝ) (f: ℝ → ℝ) (L:ℝ) (x₀:ℝ) : namespace Chapter9 -/-- Example 9.3.2 -/ -example : (5:ℝ).CloseFn (.Icc 1 3) (fun x ↦ x^2) 4 := by sorry +/-- Example 9.3.2 +Slight change from the book to accomodate the change to {lean}`Real.CloseFn` +-/ +example : (5.1:ℝ).CloseFn (.Icc 1 3) (fun x ↦ x^2) 4 := by sorry -/-- Example 9.3.2 -/ -example : (0.41:ℝ).CloseFn (.Icc 1.9 2.1) (fun x ↦ x^2) 4 := by sorry +/-- Example 9.3.2 +Slight change from the book to accomodate the change to {lean}`Real.CloseFn` +-/ +example : (0.42:ℝ).CloseFn (.Icc 1.9 2.1) (fun x ↦ x^2) 4 := by sorry /-- Example 9.3.4 -/ example: ¬(0.1:ℝ).CloseFn (.Icc 1 3) (fun x ↦ x^2) 4 := by @@ -88,91 +94,93 @@ example: Convergesto (.Icc 1 3) (fun x ↦ x^2) 4 2 := by sorry /-- Proposition 9.3.9 / Exercise 9.3.1 -/ -theorem Convergesto.iff_conv {E:Set ℝ} (f: ℝ → ℝ) (L:ℝ) {x₀:ℝ} (h: AdherentPt x₀ E) : +theorem 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) := by sorry -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₀)) : +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) := by - rw [iff_conv f L h] at hf; solve_by_elim + rw [iff_conv f L] at hf; solve_by_elim --- 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. +-- 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). /-- 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' := by -- This proof is written to follow the structure of the original text. let ⟨ a, ha, hconv ⟩ := (limit_of_AdherentPt _ _).mp h - exact tendsto_nhds_unique (hf.comp h ha hconv) (hf'.comp h ha hconv) + exact tendsto_nhds_unique (hf.comp ha hconv) (hf'.comp ha hconv) /-- Proposition 9.3.14 (Limit laws for functions) -/ -theorem Convergesto.add {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) +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₀ := by -- This proof is written to follow the structure of the original text. - rw [iff_conv _ _ h] at hf hg ⊢ + rw [iff_conv _ _] at hf hg ⊢ intro a ha hconv; specialize hf a ha hconv; specialize hg a ha hconv convert hf.add hg using 1 /-- Proposition 9.3.14 (Limit laws for functions) / Exercise 9.3.2 -/ -theorem Convergesto.sub {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) +theorem 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₀ := by sorry /-- Proposition 9.3.14 (Limit laws for functions) / Exercise 9.3.2 -/ -theorem Convergesto.max {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) +theorem 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₀ := by sorry /-- Proposition 9.3.14 (Limit laws for functions) / Exercise 9.3.2 -/ -theorem Convergesto.min {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) +theorem 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₀ := by sorry /-- Proposition 9.3.14 (Limit laws for functions) / Exercise 9.3.2 -/ -theorem Convergesto.smul {E:Set ℝ} {f: ℝ → ℝ} {L:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) +theorem Convergesto.smul {E:Set ℝ} {f: ℝ → ℝ} {L:ℝ} {x₀:ℝ} (hf: Convergesto E f L x₀) (c:ℝ) : Convergesto E (c • f) (c * L) x₀ := by sorry /-- Proposition 9.3.14 (Limit laws for functions) / Exercise 9.3.2 -/ -theorem Convergesto.mul {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) +theorem 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₀ := by sorry /-- 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 Convergesto.div {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) (hM: M ≠ 0) +theorem 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₀ := by sorry -theorem Convergesto.const {E:Set ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) (c:ℝ) - : Convergesto E (fun x ↦ c) c x₀ := by +theorem Convergesto.const (E:Set ℝ) (x₀:ℝ) (c:ℝ) + : Convergesto E (fun _ ↦ c) c x₀ := by sorry -theorem Convergesto.id {E:Set ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) +theorem Convergesto.id (E:Set ℝ) (x₀:ℝ) : Convergesto E (fun x ↦ x) x₀ x₀ := by sorry -theorem Convergesto.sq {E:Set ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) - : Convergesto E (fun x ↦ x^2) x₀ (x₀^2) := by +theorem Convergesto.sq (E:Set ℝ) (x₀:ℝ) + : Convergesto E (fun x ↦ x^2) (x₀^2) x₀ := by sorry -theorem Convergesto.linear {E:Set ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) (c:ℝ) - : Convergesto E (fun x ↦ c * x) x₀ (c * x₀) := by +theorem Convergesto.linear (E:Set ℝ) (x₀:ℝ) (c:ℝ) + : Convergesto E (fun x ↦ c * x) (c * x₀) x₀ := by sorry -theorem 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) := by +theorem Convergesto.quadratic (E:Set ℝ) (x₀:ℝ) (c d:ℝ) + : Convergesto E (fun x ↦ x^2 + c * x + d) (x₀^2 + c * x₀ + d) x₀ := by sorry -theorem 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₀ := by +theorem Convergesto.restrict {X Y:Set ℝ} {f: ℝ → ℝ} {L:ℝ} {x₀:ℝ} (hf: Convergesto X f L x₀) (hY: Y ⊆ X) : Convergesto Y f L x₀ := by sorry theorem Real.sign_def (x:ℝ) : Real.sign x = if x < 0 then -1 else if x > 0 then 1 else 0 := rfl @@ -193,7 +201,7 @@ theorem Convergesto.f_9_3_17_remove : Convergesto (.univ \ {0}) f_9_3_17 0 0 := theorem Convergesto.f_9_3_17_all : ¬ ∃ L, Convergesto .univ f_9_3_17 L 0 := by sorry /-- Proposition 9.3.18 / Exercise 9.3.3 -/ -theorem Convergesto.local {E:Set ℝ} {f: ℝ → ℝ} {L:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) {δ:ℝ} (hδ: δ > 0) : +theorem Convergesto.local {E:Set ℝ} {f: ℝ → ℝ} {L:ℝ} {x₀:ℝ} {δ:ℝ} (hδ: δ > 0) : Convergesto E f L x₀ ↔ Convergesto (E ∩ .Ioo (x₀-δ) (x₀+δ)) f L x₀ := by sorry @@ -216,7 +224,7 @@ example : ¬ ∃ L, Convergesto .univ f_9_3_21 L 0 := by sorry /- 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 Convergesto.squeeze {E:Set ℝ} {f g h: ℝ → ℝ} {L:ℝ} {x₀:ℝ} (had: AdherentPt x₀ E) +theorem 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₀ := by diff --git a/Analysis/Section_9_4.lean b/Analysis/Section_9_4.lean index 35affd11..2866b47d 100644 --- a/Analysis/Section_9_4.lean +++ b/Analysis/Section_9_4.lean @@ -79,35 +79,35 @@ theorem _root_.Filter.Tendsto.comp_of_continuous {X:Set ℝ} {f: ℝ → ℝ} {x theorem ContinuousWithinAt.add {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ} (h : x₀ ∈ X) (hf: ContinuousWithinAt f X x₀) (hg: ContinuousWithinAt g X x₀) : ContinuousWithinAt (f + g) X x₀ := by - rw [iff] at hf hg ⊢; convert hf.add (AdherentPt.of_mem h) hg using 1 + rw [iff] at hf hg ⊢; convert hf.add hg using 1 theorem ContinuousWithinAt.sub {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ} (h : x₀ ∈ X) (hf: ContinuousWithinAt f X x₀) (hg: ContinuousWithinAt g X x₀) : ContinuousWithinAt (f - g) X x₀ := by - rw [iff] at hf hg ⊢; convert hf.sub (AdherentPt.of_mem h) hg using 1 + rw [iff] at hf hg ⊢; convert hf.sub hg using 1 theorem ContinuousWithinAt.max {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ} (h : x₀ ∈ X) (hf: ContinuousWithinAt f X x₀) (hg: ContinuousWithinAt g X x₀) : ContinuousWithinAt (max f g) X x₀ := by - rw [iff] at hf hg ⊢; convert hf.max (AdherentPt.of_mem h) hg using 1 + rw [iff] at hf hg ⊢; convert hf.max hg using 1 theorem ContinuousWithinAt.min {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ} (h : x₀ ∈ X) (hf: ContinuousWithinAt f X x₀) (hg: ContinuousWithinAt g X x₀) : ContinuousWithinAt (min f g) X x₀ := by - rw [iff] at hf hg ⊢; convert hf.min (AdherentPt.of_mem h) hg using 1 + rw [iff] at hf hg ⊢; convert hf.min hg using 1 theorem ContinuousWithinAt.mul' {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ} (h : x₀ ∈ X) (hf: ContinuousWithinAt f X x₀) (hg: ContinuousWithinAt g X x₀) : ContinuousWithinAt (f * g) X x₀ := by - rw [iff] at hf hg ⊢; convert hf.mul (AdherentPt.of_mem h) hg using 1 + rw [iff] at hf hg ⊢; convert hf.mul hg using 1 theorem ContinuousWithinAt.div' {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ} (h : x₀ ∈ X) (hM: g x₀ ≠ 0) (hf: ContinuousWithinAt f X x₀) (hg: ContinuousWithinAt g X x₀) : ContinuousWithinAt (f / g) X x₀ := by - rw [iff] at hf hg ⊢; convert hf.div (AdherentPt.of_mem h) hM hg using 1 + rw [iff] at hf hg ⊢; convert hf.div hM hg using 1 /-- Proposition 9.4.10 / Exercise 9.4.3 -/ theorem Continuous.exp {a:ℝ} (ha: a>0) : Continuous (fun x:ℝ ↦ a ^ x) := by diff --git a/Analysis/Section_9_5.lean b/Analysis/Section_9_5.lean index 44694b3f..6d9674ac 100644 --- a/Analysis/Section_9_5.lean +++ b/Analysis/Section_9_5.lean @@ -64,7 +64,7 @@ theorem right_limit.conv {X: Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} (had: Adherent (hconv: Filter.atTop.Tendsto a (nhds x₀)) : Filter.atTop.Tendsto (fun n ↦ f (a n)) (nhds (right_limit X f x₀)) := by choose L hL using h - apply Convergesto.comp had _ ha hconv + apply Convergesto.comp _ ha hconv rwa [Convergesto.iff, (eq had hL).2] theorem left_limit.conv {X: Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} (had: AdherentPt x₀ (X ∩ .Iio x₀)) @@ -73,7 +73,7 @@ theorem left_limit.conv {X: Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} (had: AdherentP (hconv: Filter.atTop.Tendsto a (nhds x₀)) : Filter.atTop.Tendsto (fun n ↦ f (a n)) (nhds (left_limit X f x₀)) := by choose L hL using h - apply Convergesto.comp had _ ha hconv + apply Convergesto.comp _ ha hconv rwa [Convergesto.iff, (eq had hL).2] /-- Proposition 9.5.3 -/ diff --git a/Analysis/Section_9_6.lean b/Analysis/Section_9_6.lean index 097560fb..acc734c8 100644 --- a/Analysis/Section_9_6.lean +++ b/Analysis/Section_9_6.lean @@ -63,7 +63,7 @@ theorem BddOn.of_continuous_on_compact {a b:ℝ} (_h:a < b) {f:ℝ → ℝ} (hf: have why (j:ℕ) : n j ≥ j := why_7_6_3 hn j replace hf := hf.continuousWithinAt hLX rw [ContinuousWithinAt.iff] at hf - replace hf := hf.comp (AdherentPt.of_mem hLX) (fun j ↦ haX (n j)) hconv + replace hf := hf.comp (fun j ↦ haX (n j)) hconv apply Metric.isBounded_range_of_tendsto at hf rw [isBounded_def] at hf; choose M hpos hM using hf choose j hj using exists_nat_gt M