From 52ef55762fe184ccdc52602520f8d7a41b2f4eda Mon Sep 17 00:00:00 2001 From: Rado Kirov Date: Thu, 21 May 2026 19:16:48 -0700 Subject: [PATCH 1/3] Section 10.3: remove unused hab : a < b hypothesis Both strictMono_of_positive_derivative and strictAnti_of_negative_derivative take a < b in their signatures but the resulting StrictMonoOn / StrictAntiOn statement supplies the relevant ordering directly when applied, so this hypothesis is redundant. Co-Authored-By: Claude Opus 4.7 (1M context) --- Analysis/Section_10_3.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Analysis/Section_10_3.lean b/Analysis/Section_10_3.lean index e1ea008e6..17755a0a5 100644 --- a/Analysis/Section_10_3.lean +++ b/Analysis/Section_10_3.lean @@ -28,12 +28,12 @@ theorem derivative_of_antitone (X:Set ℝ) {x₀:ℝ} (hx₀: ClusterPt x₀ (.p sorry /-- Proposition 10.3.3 / Exercise 10.3.4 -/ -theorem strictMono_of_positive_derivative {a b:ℝ} (hab: a < b) {f:ℝ → ℝ} +theorem strictMono_of_positive_derivative {a b:ℝ} {f:ℝ → ℝ} (hderiv: DifferentiableOn ℝ f (.Icc a b)) (hpos: ∀ x ∈ Set.Ioo a b, derivWithin f (.Icc a b) x > 0) : StrictMonoOn f (.Icc a b) := by sorry -theorem strictAnti_of_negative_derivative {a b:ℝ} (hab: a < b) {f:ℝ → ℝ} +theorem strictAnti_of_negative_derivative {a b:ℝ} {f:ℝ → ℝ} (hderiv: DifferentiableOn ℝ f (.Icc a b)) (hneg: ∀ x ∈ Set.Ioo a b, derivWithin f (.Icc a b) x < 0) : StrictAntiOn f (.Icc a b) := by sorry From 4dbc4c7ea665f1f9398511aca85cbd4a749e7fc8 Mon Sep 17 00:00:00 2001 From: Rado Kirov Date: Thu, 21 May 2026 19:17:15 -0700 Subject: [PATCH 2/3] Section 10.4: remove unused hcluster from inverse_function_theorem MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The hcluster : ClusterPt x₀ (.principal (X \ {x₀})) hypothesis is not used in the proof. Same cleanup pattern as the recent Section 9.3 and 9.4 upstream commits. Co-Authored-By: Claude Opus 4.7 (1M context) --- Analysis/Section_10_4.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Analysis/Section_10_4.lean b/Analysis/Section_10_4.lean index a3ff59e04..f2c2255aa 100644 --- a/Analysis/Section_10_4.lean +++ b/Analysis/Section_10_4.lean @@ -57,7 +57,6 @@ theorem inverse_function_theorem {X Y: Set ℝ} {f: ℝ → ℝ} {g:ℝ → ℝ} (hfXY: ∀ x ∈ X, f x ∈ Y) (hgYX: ∀ y ∈ Y, g y ∈ X) (hgf: ∀ x ∈ X, g (f x) = x) (hfg: ∀ y ∈ Y, f (g y) = y) {x₀ y₀ f'x₀: ℝ} (hx₀: x₀ ∈ X) (hfx₀: f x₀ = y₀) (hne : f'x₀ ≠ 0) - (hcluster: ClusterPt x₀ (.principal (X \ {x₀}))) (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. From 638db1a193b27c5d5fdc36922a0d8c4c4a4e05f5 Mon Sep 17 00:00:00 2001 From: Rado Kirov Date: Thu, 21 May 2026 19:17:32 -0700 Subject: [PATCH 3/3] =?UTF-8?q?Section=2010.4:=20change=20.Ici=200=20?= =?UTF-8?q?=E2=86=92=20.Ioi=200=20in=20Exercises=2010.4.1=E2=80=9310.4.3?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The differentiability statements for x ↦ x^(1/n:ℝ) and friends fail at 0: the cube-root example just above (¬ DifferentiableWithinAt (·^(1/3:ℝ)) (.Ici 0) 0) demonstrates that 1/n is not always differentiable from the right at 0. The intended domain throughout these exercises is .Ioi 0; with that change the (hn: n > 0) hypothesis in 10.4.1 also becomes unnecessary (the n = 0 case gives x^(1/0) = x^0 = 1, which is constant, so the derivative formula still holds via Real's junk-value convention). Co-Authored-By: Claude Opus 4.7 (1M context) --- Analysis/Section_10_4.lean | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/Analysis/Section_10_4.lean b/Analysis/Section_10_4.lean index f2c2255aa..5404ef5be 100644 --- a/Analysis/Section_10_4.lean +++ b/Analysis/Section_10_4.lean @@ -73,27 +73,27 @@ theorem inverse_function_theorem {X Y: Set ℝ} {f: ℝ → ℝ} {g:ℝ → ℝ} convert (hf _ hx _).inv₀ _ using 2 with n <;> grind /-- Exercise 10.4.1(a) -/ -example {n:ℕ} (hn: n > 0) : ContinuousOn (fun x:ℝ ↦ x^(1/n:ℝ)) (.Ici 0) := by sorry +example {n:ℕ} : ContinuousOn (fun x:ℝ ↦ x^(1/n:ℝ)) (.Ioi 0) := by sorry /-- Exercise 10.4.1(b) -/ -example {n:ℕ} (hn: n > 0) {x:ℝ} (hx: x ∈ Set.Ici 0) : HasDerivWithinAt (fun x:ℝ ↦ x^(1/n:ℝ)) - ((n:ℝ)⁻¹ * x^((n:ℝ)⁻¹-1)) (.Ici 0) x := by sorry +example {n:ℕ} {x:ℝ} (hx: x ∈ Set.Ioi 0) : HasDerivWithinAt (fun x:ℝ ↦ x^(1/n:ℝ)) + ((n:ℝ)⁻¹ * x^((n:ℝ)⁻¹-1)) (.Ioi 0) x := by sorry /-- Exercise 10.4.2(a) -/ -example (q:ℚ) {x:ℝ} (hx: x ∈ Set.Ici 0) : - HasDerivWithinAt (fun x:ℝ ↦ x^(q:ℝ)) (q * x^(q-1:ℝ)) (.Ici 0) x := by +example (q:ℚ) {x:ℝ} (hx: x ∈ Set.Ioi 0) : + HasDerivWithinAt (fun x:ℝ ↦ x^(q:ℝ)) (q * x^(q-1:ℝ)) (.Ioi 0) x := by sorry /-- Exercise 10.4.2(b) -/ -example (q:ℚ) : (nhdsWithin 1 (.Ici 0 \ {1})).Tendsto (fun x:ℝ ↦ (x^(q:ℝ)-1)/(x-1)) (nhds q) := by +example (q:ℚ) : (nhdsWithin 1 (.Ioi 0 \ {1})).Tendsto (fun x:ℝ ↦ (x^(q:ℝ)-1)/(x-1)) (nhds q) := by sorry /-- Exercise 10.4.3(a) -/ -example (α:ℝ) : (nhdsWithin 1 (.Ici 0 \ {1})).Tendsto (fun x:ℝ ↦ (x^α-1^α)/(x-1)) (nhds α) := by +example (α:ℝ) : (nhdsWithin 1 (.Ioi 0 \ {1})).Tendsto (fun x:ℝ ↦ (x^α-1^α)/(x-1)) (nhds α) := by sorry /-- Exercise 10.4.3(b) -/ -example (α:ℝ) {x:ℝ} (hx: x ∈ Set.Ici 0) : HasDerivWithinAt (fun x:ℝ ↦ x^α) (α * x^(α-1)) (.Ici 0) x := by +example (α:ℝ) {x:ℝ} (hx: x ∈ Set.Ioi 0) : HasDerivWithinAt (fun x:ℝ ↦ x^α) (α * x^(α-1)) (.Ioi 0) x := by sorry end Chapter10