typos fixes and removal of unneed hypothesis - 10.3 10.4#503
Merged
Conversation
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) <noreply@anthropic.com>
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) <noreply@anthropic.com>
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) <noreply@anthropic.com>
rkirov
commented
May 22, 2026
|
|
||
| /-- 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:ℝ → ℝ} |
Contributor
Author
There was a problem hiding this comment.
vacuously true even if a < b is not true.
rkirov
commented
May 22, 2026
|
|
||
| /-- 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 |
Contributor
Author
There was a problem hiding this comment.
n = 0 is true due to garbage value of 1 / n but I can see an argument to keeping it even if not used in proof.
The Ici to Ioi change is just fixing a typo.
rkirov
commented
May 22, 2026
| (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₀}))) |
Contributor
Author
There was a problem hiding this comment.
This assumption is not needed. Full proof without it - https://github.com/rkirov/analysis/blob/main/Analysis/Section_10_4.lean#L81-L113
rkirov
changed the title
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.