feat(MeasureTheory.VectorMeasure): add several lemmas which characterize variation#26160
Open
oliver-butterley wants to merge 143 commits intoleanprover-community:masterfrom
Open
feat(MeasureTheory.VectorMeasure): add several lemmas which characterize variation#26160oliver-butterley wants to merge 143 commits intoleanprover-community:masterfrom
oliver-butterley wants to merge 143 commits intoleanprover-community:masterfrom
Conversation
This reverts commit e2b20d9.
…utterley/Variation
yoh-tanimoto
removed
the
awaiting-author
EtienneC30
reviewed
Mar 31, 2026
Member
EtienneC30
left a comment
EtienneC30
left a comment
There was a problem hiding this comment.
Here is a new round of comments:
EtienneC30
reviewed
Mar 31, 2026
EtienneC30
added
the
awaiting-author
Co-authored-by: Etienne Marion <[email protected]>
Co-authored-by: Etienne Marion <[email protected]>
yoh-tanimoto
removed
the
awaiting-author
EtienneC30
reviewed
Apr 2, 2026
EtienneC30
added
the
awaiting-author
EtienneC30
reviewed
Apr 2, 2026
| ne_eq, and_imp] | ||
| grind | ||
| calc | ||
| ∑ p ∈ P, ‖μ p‖ₑ = ∑ p ∈ Q.parts, ‖μ p‖ₑ := by |
Member
There was a problem hiding this comment.
As there are already several lemmas about sums in the Finpartition file, maybe this should go there as well after the definition of ofPairwiseDisjoint.
Collaborator
There was a problem hiding this comment.
defined sum_ofPairwiseDisjoint_eq_sum and sum_ofSubset_eq_sum.
Co-authored-by: Etienne Marion <[email protected]>
yoh-tanimoto
removed
the
awaiting-author
EtienneC30
added
the
awaiting-author
Co-authored-by: Etienne Marion <[email protected]>
yoh-tanimoto
removed
the
awaiting-author
EtienneC30
reviewed
Apr 4, 2026
Comment on lines
+18
to
+19
| When `μ` is a signed measure, it will be shown that `μ.variation E = μ.totalVariation E`. When `μ` | ||
| is `ℝ≥0∞`-valued measure, `μ.variation` coincides with `μ` on measurable sets. |
Member
There was a problem hiding this comment.
This is not in the PR, correct? If so, please either add this as a TODO, or remove it if you are already working on it.
Collaborator
EtienneC30
added
the
awaiting-author
Co-authored-by: Etienne Marion <[email protected]>
yoh-tanimoto
removed
the
awaiting-author
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
7 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.
Add the following lemmas concerning variation of a VectorMeasure:
norm_measure_le_variation:‖μ E‖ₑ ≤ variation μ E.variation_neg:(-μ).variation = μ.variation.variation_zero:(0 : VectorMeasure X V).variation = 0.absolutelyContinuousCo-authored-by: @yoh-tanimoto