feat(MeasureTheory): prove Exercise 1.1.1 (Boolean closure of elementary sets) - #662
Open
Chessing234 wants to merge 7 commits into
Open
feat(MeasureTheory): prove Exercise 1.1.1 (Boolean closure of elementary sets)#662Chessing234 wants to merge 7 commits into
Chessing234 wants to merge 7 commits into
Conversation
Both fall straight out of the definition: a union of two finite unions of boxes is indexed by the union of the two finsets, and the empty set by the empty finset. Moves `empty` above `union'`, which needs it for the base case of the induction in the next commit.
Induction on the finset: the empty union is the empty set, and an `insert a S'` union is `a` united with the union over `S'`, which is elementary by `IsElementary.union`.
The intersection of two boxes is the box whose sides are the pairwise intersections of the sides, which `BoundedInterval.inter` already provides; that is worth stating on its own as `Box.inter`. Intersecting the two finite unions then distributes over the product of the two finsets, so the witness is the image of `S ×ˢ T` under the pairwise-intersection map.
`I \ J` is the part of `I` below `J` together with the part above it, and each of those is again a bounded interval. Writing that down needs a way to build an interval from its endpoints and two open/closed flags, so add `BoundedInterval.mk'` with the corresponding accessors, plus `lclosed` and `uclosed` and a membership lemma phrased in terms of them. The two pieces are intersected with `I` via `BoundedInterval.inter`, which keeps them inside `I` when `J` lies entirely outside it.
A point of `B \ C` leaves `C` in some coordinate, so `B \ C` is the union over the coordinates of the boxes obtained from `B` by shrinking that side to one of the two pieces of the interval difference - a finite union of boxes, i.e. `Box.sdiff`. `E \ F` then follows by induction on the boxes of `F`: removing one box from an elementary set removes it from each of its boxes, and the results are collected by `IsElementary.union'`. The symmetric difference is the union of the two differences.
Translating an interval shifts both endpoints and keeps each end open or closed, which `mk'` states directly; a box translates coordinatewise, and an elementary set by translating each box of a representation.
The build job failed on `curl: (35) Recv failure: Connection reset by peer` while the runner installed elan, before any Lean ran.
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.
Fills the seven
sorrys of Exercise 1.1.1 inAnalysis/MeasureTheory/Section_1_1_1.lean:IsElementary.union,.union',.empty,.inter,.sdiff,.symmDiffand.translate. Six commits, one idea each.Three supporting lemmas were needed and are stated on their own:
Box.inter— the intersection of two boxes is the box of the pairwise side intersections, using the existingBoundedInterval.inter;BoundedInterval.sdiff—I \ Jis the part ofIbelowJunion the part above it. Expressing those needed a constructor from endpoints plus open/closed flags, so this addsBoundedInterval.mk'withlclosed/uclosedaccessors and a membership lemma. Both pieces are intersected withI, which matters whenJmissesIentirely;Box.sdiff— a point ofB \ CleavesCin some coordinate, soB \ Cis the union over coordinates ofBwith that side shrunk to one of the two pieces, andBox.translate, mirroring the construction already used later inBox.volume_of_translate.E \ Fis then an induction over the boxes ofF, andsymmDiffis the union of the two differences.lake build Analysis.MeasureTheory.Section_1_1_1→Build completed successfully (3279 jobs)., with no warnings, and the file'ssorrycount drops from 13 to 6. Every commit builds on its own.