fix: Exercise 1.2.2' should assume uniform convergence on [0,1] - #649
Open
Chessing234 wants to merge 1 commit into
Open
fix: Exercise 1.2.2' should assume uniform convergence on [0,1]#649Chessing234 wants to merge 1 commit into
Chessing234 wants to merge 1 commit into
Conversation
`Ex_1_2_2b` stated the uniform-convergence hypothesis as ∀ x ∈ Set.Icc 0 1, TendstoUniformly f F Filter.atTop `TendstoUniformly f F atTop` already quantifies over the whole domain, so the bound variable `x` does not occur in its body: the binder is vacuous, and what the hypothesis actually demands is uniform convergence on all of ℝ. Every other hypothesis and the conclusion are scoped to `Icc 0 1`, and Exercise 1.2.2' asks about uniform convergence on `[0,1]`, so use `TendstoUniformlyOn f F Filter.atTop (Set.Icc 0 1)`. The intended answer is unchanged -- a uniform limit of Riemann integrable functions on [0,1] is Riemann integrable either way -- but the old form assumed strictly more than the exercise gives you. Also wrap the statement to the 100-character limit; it was 284.
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
1 participant
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.
Ex_1_2_2b(Exercise 1.2.2') states the uniform-convergence hypothesis asTendstoUniformly f F Filter.atTopalready quantifies over the whole domain, soxdoes not occur in the body of that binder. Two consequences:∀ x ∈ Set.Icc 0 1is vacuous — moduloIcc 0 1being nonempty it is justthe inner proposition;
other hypothesis and the conclusion are scoped to
Icc 0 1.Exercise 1.2.2' asks whether uniform convergence on [0,1] of uniformly bounded
Riemann integrable functions preserves Riemann integrability, so the hypothesis
should be
TendstoUniformlyOn f F Filter.atTop (Set.Icc 0 1).The intended answer does not change — a uniform limit of Riemann integrable
functions on [0,1] is Riemann integrable, so this is still
isTrue— but the oldform hands the solver a strictly stronger hypothesis than the exercise offers,
and states it about the wrong set.
I also wrapped the declaration to the 100-character limit from CONTRIBUTING; it
was a single 284-character line, and the neighbouring
examplefor Exercise1.2.2 is already wrapped the same way.
No Lean toolchain build was run for this — relying on the build CI on this PR.