From 76cf7ab1c08fae7153d257e34a968bd5e41fe9ae Mon Sep 17 00:00:00 2001 From: Rado Kirov Date: Fri, 10 Apr 2026 20:58:53 -0700 Subject: [PATCH 1/2] 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 From d00ba167b80fe231daaf7ddbb65376859ca6bb99 Mon Sep 17 00:00:00 2001 From: Rado Kirov Date: Sun, 19 Apr 2026 16:09:12 -0700 Subject: [PATCH 2/2] =?UTF-8?q?Section=209.4:=20remove=20unused=20x?= =?UTF-8?q?=E2=82=80=20=E2=88=88=20X=20hypotheses=20and=20fix=20Continuous?= =?UTF-8?q?WithinAt.comp=20typo?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Follow-up to the AdherentPt removal: once `AdherentPt.of_mem h` is no longer called in the bodies of `ContinuousWithinAt.add/.sub/.max/.min/ .mul'/.div'`, the `(h : x₀ ∈ X)` hypothesis is unused. Drop it. Same cleanup for `Filter.Tendsto.comp_of_continuous` and for `ContinuousWithinAt.tfae` (also makes `x₀` explicit there, since there is no longer a hypothesis to infer it from). Drop the stale "It is possible that the hypothesis x₀ ∈ X is unnecessary" comment. `ContinuousWithinAt.comp` had `(hx₀: x ∈ X)` where `x` was an auto-bound implicit (not `x₀`), so the hypothesis was a latent typo. Remove it and make `x₀` explicit. Update cascaded call sites in 9.5, 9.6, 9.7, 9.9, 10.4, 11.9. Co-Authored-By: Claude Opus 4.7 (1M context) --- Analysis/Section_10_4.lean | 2 +- Analysis/Section_11_9.lean | 2 +- Analysis/Section_9_4.lean | 24 +++++++++++++----------- Analysis/Section_9_5.lean | 2 +- Analysis/Section_9_6.lean | 2 +- Analysis/Section_9_7.lean | 2 +- Analysis/Section_9_9.lean | 4 ++-- 7 files changed, 20 insertions(+), 18 deletions(-) diff --git a/Analysis/Section_10_4.lean b/Analysis/Section_10_4.lean index a7d5f491..fd31378c 100644 --- a/Analysis/Section_10_4.lean +++ b/Analysis/Section_10_4.lean @@ -68,7 +68,7 @@ theorem inverse_function_theorem {X Y: Set ℝ} {f: ℝ → ℝ} {g:ℝ → ℝ} have hy₀: y₀ ∈ Y := by aesop have hx : ∀ n, x n ∈ X \ {x₀}:= by sorry - replace hconv := hconv.comp_of_continuous hy₀ hg hy' + replace hconv := hconv.comp_of_continuous hg hy' have hgy₀ : g y₀ = x₀ := by aesop rw [HasDerivWithinAt.iff, ←Convergesto.iff, Convergesto.iff_conv _ _] at hf convert (hf _ hx _).inv₀ _ using 2 with n <;> grind diff --git a/Analysis/Section_11_9.lean b/Analysis/Section_11_9.lean index 002ed0c1..a836c3e3 100644 --- a/Analysis/Section_11_9.lean +++ b/Analysis/Section_11_9.lean @@ -73,7 +73,7 @@ theorem deriv_of_integ {a b:ℝ} (hab: a < b) {f:ℝ → ℝ} (hf: IntegrableOn HasDerivWithinAt (fun x => integ f (Icc a x)) (f x₀) (.Icc a b) x₀ := by -- This proof is written to follow the structure of the original text. rw [HasDerivWithinAt.iff_approx_linear] - simp [(ContinuousWithinAt.tfae _ f hx₀).out 0 2] at hcts + simp [(ContinuousWithinAt.tfae _ f x₀).out 0 2] at hcts peel hcts with ε hε δ hδ hconv; intro y hy hyδ obtain hx₀y | rfl | hx₀y := lt_trichotomy x₀ y . have := ((hf.join (join_Icc_Ioc hy.1 hy.2)).1.join (join_Icc_Ioc hx₀.1 (le_of_lt hx₀y))).2 diff --git a/Analysis/Section_9_4.lean b/Analysis/Section_9_4.lean index 2866b47d..766428db 100644 --- a/Analysis/Section_9_4.lean +++ b/Analysis/Section_9_4.lean @@ -58,8 +58,8 @@ example : ¬ ContinuousAt f_9_4_6 0 := by sorry example : ContinuousWithinAt f_9_4_6 (.Ici 0) 0 := by sorry -/-- Proposition 9.4.7 / Exercise 9.4.1. It is possible that the hypothesis {lean}`x₀ ∈ X` is unnecessary. -/ -theorem ContinuousWithinAt.tfae (X:Set ℝ) (f: ℝ → ℝ) {x₀:ℝ} (h : x₀ ∈ X) : +/-- Proposition 9.4.7 / Exercise 9.4.1. -/ +theorem ContinuousWithinAt.tfae (X:Set ℝ) (f: ℝ → ℝ) (x₀:ℝ) : [ ContinuousWithinAt f X x₀, ∀ a:ℕ → ℝ, (∀ n, a n ∈ X) → Filter.atTop.Tendsto a (nhds x₀) → Filter.atTop.Tendsto (fun n ↦ f (a n)) (nhds (f x₀)), @@ -68,43 +68,43 @@ theorem ContinuousWithinAt.tfae (X:Set ℝ) (f: ℝ → ℝ) {x₀:ℝ} (h : x sorry /-- Remark 9.4.8 --/ -theorem _root_.Filter.Tendsto.comp_of_continuous {X:Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} (h : x₀ ∈ X) +theorem _root_.Filter.Tendsto.comp_of_continuous {X:Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} (h_cont: ContinuousWithinAt f X x₀) {a: ℕ → ℝ} (ha: ∀ n, a n ∈ X) (hconv: Filter.atTop.Tendsto a (nhds x₀)): Filter.atTop.Tendsto (fun n ↦ f (a n)) (nhds (f x₀)) := by - have := (ContinuousWithinAt.tfae X f h).out 0 1 + have := (ContinuousWithinAt.tfae X f x₀).out 0 1 grind /- Proposition 9.4.9 -/ -theorem ContinuousWithinAt.add {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ} (h : x₀ ∈ X) +theorem ContinuousWithinAt.add {X:Set ℝ} (f g: ℝ → ℝ) {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 hg using 1 -theorem ContinuousWithinAt.sub {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ} (h : x₀ ∈ X) +theorem ContinuousWithinAt.sub {X:Set ℝ} (f g: ℝ → ℝ) {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 hg using 1 -theorem ContinuousWithinAt.max {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ} (h : x₀ ∈ X) +theorem ContinuousWithinAt.max {X:Set ℝ} (f g: ℝ → ℝ) {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 hg using 1 -theorem ContinuousWithinAt.min {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ} (h : x₀ ∈ X) +theorem ContinuousWithinAt.min {X:Set ℝ} (f g: ℝ → ℝ) {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 hg using 1 -theorem ContinuousWithinAt.mul' {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ} (h : x₀ ∈ X) +theorem ContinuousWithinAt.mul' {X:Set ℝ} (f g: ℝ → ℝ) {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 hg using 1 -theorem ContinuousWithinAt.div' {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ} (h : x₀ ∈ X) (hM: g x₀ ≠ 0) +theorem ContinuousWithinAt.div' {X:Set ℝ} (f g: ℝ → ℝ) {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 hM hg using 1 @@ -122,7 +122,9 @@ theorem Continuous.abs : Continuous (fun x:ℝ ↦ |x|) := by sorry -- TODO /-- Proposition 9.4.13 / Exercise 9.4.5 -/ -theorem ContinuousWithinAt.comp {X Y: Set ℝ} {f g:ℝ → ℝ} (hf: ∀ x ∈ X, f x ∈ Y) {x₀:ℝ} (hx₀: x ∈ X) (hf_cont: ContinuousWithinAt f X x₀) (hg_cont: ContinuousWithinAt g Y (f x₀)): ContinuousWithinAt (g ∘ f) X x₀ := by sorry +theorem ContinuousWithinAt.comp {X Y: Set ℝ} {f g:ℝ → ℝ} (hf: ∀ x ∈ X, f x ∈ Y) (x₀:ℝ) + (hf_cont: ContinuousWithinAt f X x₀) (hg_cont: ContinuousWithinAt g Y (f x₀)): + ContinuousWithinAt (g ∘ f) X x₀ := by sorry /-- Example 9.4.14 -/ example : Continuous (fun x:ℝ ↦ 3*x + 1) := by diff --git a/Analysis/Section_9_5.lean b/Analysis/Section_9_5.lean index 6d9674ac..b4411315 100644 --- a/Analysis/Section_9_5.lean +++ b/Analysis/Section_9_5.lean @@ -85,7 +85,7 @@ theorem ContinuousAt.iff_eq_left_right_limit {X: Set ℝ} {f: ℝ → ℝ} {x₀ . sorry intro ⟨ ⟨ hre, hright⟩, ⟨ hle, lheft ⟩ ⟩ set L := f x₀ - have := (ContinuousWithinAt.tfae X f h).out 0 2 + have := (ContinuousWithinAt.tfae X f x₀).out 0 2 rw [this] intro ε hε apply right_limit.eq' at hre diff --git a/Analysis/Section_9_6.lean b/Analysis/Section_9_6.lean index acc734c8..a684e0eb 100644 --- a/Analysis/Section_9_6.lean +++ b/Analysis/Section_9_6.lean @@ -109,7 +109,7 @@ theorem IsMaxOn.of_continuous_on_compact {a b:ℝ} (h:a < b) {f:ℝ → ℝ} (hf use xmax, hmax have hn_lower (j:ℕ) : n j ≥ j := why_7_6_3 hn j have hconv' : Filter.atTop.Tendsto (fun j ↦ f (x (n j))) (nhds (f xmax)) := - hconv.comp_of_continuous hmax (hf.continuousWithinAt hmax) (fun j ↦ hx (n j)) + hconv.comp_of_continuous (hf.continuousWithinAt hmax) (fun j ↦ hx (n j)) have hlower (j:ℕ) : m - 1/(j+1:ℝ) < f (x (n j)) := by apply lt_of_le_of_lt _ (hfx (n j)); gcongr; grind have hupper (j:ℕ) : f (x (n j)) ≤ m := by apply claim1; simp [Set.mem_image, E]; use x (n j), hx (n j) diff --git a/Analysis/Section_9_7.lean b/Analysis/Section_9_7.lean index b671a9e1..e5a20561 100644 --- a/Analysis/Section_9_7.lean +++ b/Analysis/Section_9_7.lean @@ -54,7 +54,7 @@ theorem intermediate_value {a b:ℝ} (hab: a < b) {f:ℝ → ℝ} (hf: Continuou . exact tendsto_const_nhds . exact fun n ↦ le_of_lt (hx2 n) exact fun n ↦ le_csSup hE_bdd (hx1 n) - replace := this.comp_of_continuous hc (hf.continuousWithinAt hc) (fun n ↦ hE (hx1 n)) + replace := this.comp_of_continuous (hf.continuousWithinAt hc) (fun n ↦ hE (hx1 n)) have hfxny (n:ℕ) : f (x n) ≤ y := by specialize hx1 n; simp [E] at hx1; grind exact le_of_tendsto' this hfxny have hne : c < b := by grind diff --git a/Analysis/Section_9_9.lean b/Analysis/Section_9_9.lean index 368ecb4a..54836dd4 100644 --- a/Analysis/Section_9_9.lean +++ b/Analysis/Section_9_9.lean @@ -201,7 +201,7 @@ theorem UniformContinuousOn.of_continuousOn {a b:ℝ} {f:ℝ → ℝ} observe hbounded : Bornology.IsBounded (.Icc a b) have ⟨ j, hj, ⟨ L, hL, hconv⟩ ⟩ := (Heine_Borel (.Icc a b)).mp ⟨ hclosed, hbounded ⟩ _ hxmem replace hcont := ContinuousOn.continuousWithinAt hcont hL - have hconv' := hconv.comp_of_continuous hL hcont (fun k ↦ hxmem (j k)) + have hconv' := hconv.comp_of_continuous hcont (fun k ↦ hxmem (j k)) rw [Sequence.equiv_iff] at hequiv replace hequiv : atTop.Tendsto (fun k ↦ x (n (j k)) - y (n (j k))) (nhds 0) := by observe hj' : atTop.Tendsto j .atTop @@ -212,7 +212,7 @@ theorem UniformContinuousOn.of_continuousOn {a b:ℝ} {f:ℝ → ℝ} convert hconv.sub hequiv with k . abel simp - replace hyconv := hyconv.comp_of_continuous hL hcont (fun k ↦ hymem (j k)) + replace hyconv := hyconv.comp_of_continuous hcont (fun k ↦ hymem (j k)) have : atTop.Tendsto (fun k ↦ f (x (n (j k))) - f (y (n (j k)))) (nhds 0) := by convert hconv'.sub hyconv; simp sorry