feat(MeasureTheory): elementary sets are Jordan measurable - #663
Open
Chessing234 wants to merge 4 commits into
Open
feat(MeasureTheory): elementary sets are Jordan measurable#663Chessing234 wants to merge 4 commits into
Chessing234 wants to merge 4 commits into
Conversation
… hypothesis Both lemmas take a subset hypothesis relating `A` to `E` and then state a bound about `A` alone, so `hAE` is unused and neither says anything about `E`. That makes them useless for what they exist for - bounding the inner and outer measures of a set by the elementary sets around it. State them about `E`. The inner one needs `E` bounded, since otherwise the supremum ranges over an unbounded family; the outer one needs nothing extra, as the family is bounded below by zero. The old statements survive as `le_Jordan_inner_self` and `Jordan_outer_le_self` with their original proofs: they are the `A = E` case, which is all the existing call sites in Section_1_2_0 and Section_1_2_1 use, and those keep working unchanged either way.
Jordan measurability is boundedness together with agreement of the inner and outer measures, so this is needed before any of it. A box lies in the closed ball whose radius is the norm of its largest-endpoint corner, and a finite union of bounded sets is bounded.
…same measure With the two bounds now stated about the set they constrain, this is a sandwich: the outer measure is at most the elementary measure (take the set itself as the cover), which is at most the inner measure (take it as the inscribed set), and the inner measure is at most the outer. The empty set follows as the elementary set of measure zero.
Section_1_2_1 carried its own copy, a thousand lines into a later chapter, where nothing before it could use the fact - which is why this branch needed the lemma stated again. One copy, in the section that introduces elementary sets.
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.
Four
sorrys inAnalysis/MeasureTheory/Section_1_1_2.lean—IsElementary.jordanMeasurable,JordanMeasurable.mes_of_elementary,JordanMeasurable.empty,JordanMeasurable.mes_of_empty.The interesting part is the first commit, which is a statement fix rather than a proof.
le_Jordan_innerandJordan_outer_leeach take a hypothesis relatingAtoEand then state a bound aboutAalone:hAEis unused in both, and neither says anything aboutE— so neither can be used for what the names suggest, sandwiching the measures of a set between the elementary sets inside and outside it. Restated aboutE; the inner one needsEbounded, since otherwise the supremum ranges over an unbounded family. The old statements survive asle_Jordan_inner_self/Jordan_outer_le_self(theA = Ecase), which is what the existing call sites in Section_1_2_0 and Section_1_2_1 use.With that, the four proofs are short: outer ≤ elementary measure ≤ inner, and inner ≤ outer.
The one supporting fact needed is that an elementary set is bounded. Section_1_2_1 already had
IsElementary.isBounded, a thousand lines into a later chapter where nothing earlier could reach it, so the last commit moves the fact to where elementary sets are introduced and deletes the copy.lake build Analysis.MeasureTheory.Section_1_1_2 Analysis.MeasureTheory.Section_1_2_0 Analysis.MeasureTheory.Section_1_2_1→Build completed successfully (3286 jobs)., no warnings;sorrycount in Section_1_1_2 drops from 43 to 39.