fix: drop superfluous boundedness hypothesis in Ex 1.3.8(iii)/(iv) - #645
Merged
teorth merged 1 commit intoAug 11, 2026
Merged
Conversation
RealMeasurable.aeEqual/aeLimit and their Complex twins carried an extraneous |g x| <= M / |f x| <= M (norm bound for the complex versions) hypothesis with no counterpart in Tao's Exercise 1.3.8, and RealMeasurable/ComplexMeasurable (unlike UnsignedMeasurable) impose no sign or unsignedness restriction that would make such a bound needed. Comparing against the already-correct unsigned analogues just above (UnsignedMeasurable.aeEqual/aeLimit) makes the mismatch clear: those take hg : Unsigned g / hfn : Unsigned f, because UnsignedMeasurable bakes Unsigned into its own definition, so concluding UnsignedMeasurable g needs Unsigned g re-asserted. RealMeasurable has no such built-in restriction to re-assert, so the real/complex versions need no extra hypothesis at all - the boundedness assumption looks like a stray, unrelated hypothesis rather than a deliberate port of that pattern. Dropped the four now-superfluous hypotheses.
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.
RealMeasurable.aeEqual/aeLimit and their Complex twins carried an extraneous
|g x| ≤ M/‖g x‖ ≤ Mhypothesis with no counterpart in Tao's Exercise 1.3.8, andRealMeasurable/ComplexMeasurable(unlikeUnsignedMeasurable) impose no sign/unsignedness restriction that would make such a bound needed.Comparing against the already-correct unsigned analogues just above (
UnsignedMeasurable.aeEqual/aeLimit) makes the mismatch clear: those takehg : Unsigned g/hfn : Unsigned f, becauseUnsignedMeasurablebakesUnsignedinto its own definition, so concludingUnsignedMeasurable gneedsUnsigned gre-asserted.RealMeasurablehas no such built-in restriction to re-assert, so the real/complex versions need no extra hypothesis at all — the boundedness assumption looks like a stray, unrelated hypothesis rather than a deliberate port of that pattern.Dropped the four now-superfluous hypotheses.
Note: as with my other PR open right now, I wasn't able to complete a local
lake buildthis round due to network contention on my machine — this is a minimal, statement-only change (deleting unused hypothesis binders, no proof body) checked directly against the pattern used by the neighboring, already-compiling unsigned theorems. Happy to iterate on CI (build_book.yml) feedback.