[Merged by Bors] - feat(MeasureTheory.VectorMeasure): add a definition of total variation for VectorMeasure by oliver-butterley · Pull Request #26156 · leanprover-community/mathlib4

oliver-butterley · 2025-06-19T13:25:41Z

This PR adds variation for any VectorMeasure using a supremum definition. Currently mathlib has TotalVariation defined for a signed measure using the Hahn-Jordan decomposition, but this doesn't generalise.

Motivation: generally this is an important concept but specifically as a step for proving RMK in the complex case which in turn is a step to prove the spectral theorem.

Co-authored-by: @yoh-tanimoto

This PR was migrated from #25442. PR divided into smaller pieces, this is just the definition without additional lemmas. PRs adding further results related to variation are:

feat(MeasureTheory.VectorMeasure): add several lemmas which characterize variation #26160
feat(MeasureTheory.VectorMeasure): add lemma which shows that variation of a ℝ≥0∞ VectorMeasure is equal to itself #26165
feat(MeasureTheory.VectorMeasure): variation defined as a supremum is equal to variation defined using the Hahn-Jordan decomposition #26168 (shows that for SignedMeasures the two definitions of variation coincide)

This reverts commit e2b20d9.

…utterley/Variation

Co-authored-by: Sebastien Gouezel <[email protected]>

oliver-butterley · 2026-02-03T00:42:15Z

Almost everything in the file is about creating a measure (in the usual sense) from a subadditive function, right? If so, I think it would better fit as a general construction mechanism, in a dedicated file in the Measure folder. Then the specific case of the variation of a vector measure would indeed be in the VectorMeasure folder, but for now it would be a very short file (to be expanded later on with more API). What do you think?

Yes, almost the entirety of the file is creating a measure from any subadditive function. I've moved this part to a separate file and now Defs.lean is a rather short file, using the other for an almost immediate definition of variation.

sgouezel · 2026-02-03T18:03:58Z

Don't forget to remove awaiting-author when you're done, otherwise it won't show up on my queue.

yoh-tanimoto · 2026-02-03T18:45:48Z

We are unsure about the naming preVariationAux. I'm thinking whether it makes sense to combine it with IsSigmaSubadditive and define something like

structure preVariation' where
  toFun : Set Z → ℝ≥0∞
  eq_iSup_sum (s : Set Z) :
    toFun s = if h : MeasurableSet s then
                ⨆ (P : Finpartition (⟨s, h⟩ : Subtype MeasurableSet)), ∑ p ∈ P.parts, toFun p
              else 0
  isSigmaSubadditive' :
    ∀ (s : ℕ → {t : Set Z // MeasurableSet t}), Pairwise (Disjoint on (Subtype.val ∘ s)) →
      toFun (⋃ i, (s i).val) ≤ ∑' i, toFun (s i)

sgouezel · 2026-02-07T07:52:45Z

I'm confused about your question about the structure: you have a function toFun in there, but I don't understand if it's the function f from the original PR or the function preVariationAux f. The field eq_iSup_sum seems to say it's preVariationAux f, but the field isSigmaSubadditive' seems to say it's f (because the subadditivity is a property of the original function f). I think the current design, with the construction of preVariationAux f, and then additional properties under the assumption of subadditivity, is a good one. As for the naming, you could use preVariationFun for the function instead of preVariationAux, it conveys better the fact that it's only a function for now. I'm not a big fan of IsSigmaSubadditive because there are many objects in measure theory that are sigma subadditive. Maybe IsSigmaSubadditiveSetFun?

yoh-tanimoto · 2026-02-09T09:40:49Z

yes, you are absolutely right, I was confused between f and preVariation f.

I renamed as you suggested.

fpvandoorn

A few minor comments, otherwise LGTM

bors d+

Mathlib/Order/Partition/Finpartition.lean

mathlib-bors · 2026-02-10T14:24:50Z

✌️ oliver-butterley can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Co-authored-by: Floris van Doorn <[email protected]>

yoh-tanimoto · 2026-02-10T16:51:11Z

bors r+

mathlib-bors · 2026-02-10T16:51:14Z

🔒 Permission denied

Existing reviewers: click here to make yoh-tanimoto a reviewer

oliver-butterley · 2026-02-10T16:56:33Z

bors r+

@yoh-tanimoto

…n for VectorMeasure (#26156) This PR adds variation for any `VectorMeasure` using a supremum definition. Currently mathlib has `TotalVariation` defined for a signed measure using the Hahn-Jordan decomposition, but this doesn't generalise. Motivation: generally this is an important concept but specifically as a step for proving RMK in the complex case which in turn is a step to prove the spectral theorem. This PR was migrated from #25442. PR divided into smaller pieces, this is just the definition without additional lemmas. PRs adding further results related to variation are: * #26160 * #26165 * #26168 (shows that for `SignedMeasures` the two definitions of variation coincide) Co-authored-by: @yoh-tanimoto Co-authored-by: Yoh Tanimoto <[email protected]> Co-authored-by: Yoh Tanimoto <[email protected]>

mathlib-bors · 2026-02-10T18:24:50Z

Pull request successfully merged into master.

Build succeeded:

@yoh-tanimoto

…n for VectorMeasure (leanprover-community#26156) This PR adds variation for any `VectorMeasure` using a supremum definition. Currently mathlib has `TotalVariation` defined for a signed measure using the Hahn-Jordan decomposition, but this doesn't generalise. Motivation: generally this is an important concept but specifically as a step for proving RMK in the complex case which in turn is a step to prove the spectral theorem. This PR was migrated from leanprover-community#25442. PR divided into smaller pieces, this is just the definition without additional lemmas. PRs adding further results related to variation are: * leanprover-community#26160 * leanprover-community#26165 * leanprover-community#26168 (shows that for `SignedMeasures` the two definitions of variation coincide) Co-authored-by: @yoh-tanimoto Co-authored-by: Yoh Tanimoto <[email protected]> Co-authored-by: Yoh Tanimoto <[email protected]>

@yoh-tanimoto

…n for VectorMeasure (leanprover-community#26156) This PR adds variation for any `VectorMeasure` using a supremum definition. Currently mathlib has `TotalVariation` defined for a signed measure using the Hahn-Jordan decomposition, but this doesn't generalise. Motivation: generally this is an important concept but specifically as a step for proving RMK in the complex case which in turn is a step to prove the spectral theorem. This PR was migrated from leanprover-community#25442. PR divided into smaller pieces, this is just the definition without additional lemmas. PRs adding further results related to variation are: * leanprover-community#26160 * leanprover-community#26165 * leanprover-community#26168 (shows that for `SignedMeasures` the two definitions of variation coincide) Co-authored-by: @yoh-tanimoto Co-authored-by: Yoh Tanimoto <[email protected]> Co-authored-by: Yoh Tanimoto <[email protected]>

@yoh-tanimoto

…n for VectorMeasure (leanprover-community#26156) This PR adds variation for any `VectorMeasure` using a supremum definition. Currently mathlib has `TotalVariation` defined for a signed measure using the Hahn-Jordan decomposition, but this doesn't generalise. Motivation: generally this is an important concept but specifically as a step for proving RMK in the complex case which in turn is a step to prove the spectral theorem. This PR was migrated from leanprover-community#25442. PR divided into smaller pieces, this is just the definition without additional lemmas. PRs adding further results related to variation are: * leanprover-community#26160 * leanprover-community#26165 * leanprover-community#26168 (shows that for `SignedMeasures` the two definitions of variation coincide) Co-authored-by: @yoh-tanimoto Co-authored-by: Yoh Tanimoto <[email protected]> Co-authored-by: Yoh Tanimoto <[email protected]>

oliver-butterley added 30 commits May 30, 2025 16:40

Draft version

21aae86

trim imports

e2b20d9

Revert "trim imports"

e009f64

This reverts commit e2b20d9.

Filter.Tendsto.enorm'

5a390b5

enorm_prod_le_of_le

bed1aa6

enorm_tsum_le_tsum_enorm

6ab2d07

explicit

5b2e24d

comment in docstring

c3793f3

Merge commit 'c3793f3be149421e18bf18df612a438b9762b7e2' into oliver-b…

9bb3663

…utterley/Variation

clean

6dc88ea

Reduced assumptions

c5f96a0

variation_of_ENNReal

730777a

variation_SignedMeasure placeholder

d456743

isInnerPart_of_empty

ddebcc7

isInnerPart_self

dcdbbb6

isInnerPart_monotone

0861ff7

variables

e2bf357

placeholder statements

eb4d4a6

isInnerPart_iUnion

4321c77

isInnerPart_of_disjoint

81af146

restriction_isInnerPart

9f65dbb

supPartSum_empty'

6193c13

supSumPart_lt

729dd8b

supSumPart_le

a2eab8f

le_supSumPart

a2e614f

notes

8a4209e

var_aux

22b45b5

sum_part_le_tsum_sum_part

4b5b63b

sum_part_le_tsum_sum_part

5d7a442

isSubadditive_enorm_measure

57c8cb8

oliver-butterley and others added 5 commits February 3, 2026 00:07

Update Mathlib/MeasureTheory/VectorMeasure/Variation/Defs.lean

88d2b52

Co-authored-by: Sebastien Gouezel <[email protected]>

Update Mathlib/MeasureTheory/VectorMeasure/Variation/Defs.lean

8c08168

Co-authored-by: Sebastien Gouezel <[email protected]>

NNReal

3830704

reviewer's suggestions

7f486ad

split file

d948d8a

Update Mathlib.lean

e08522c

rename, min_imports

4912c0f

yoh-tanimoto removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 9, 2026

fpvandoorn approved these changes Feb 10, 2026

View reviewed changes

Mathlib/Order/Partition/Finpartition.lean Outdated Show resolved Hide resolved

Mathlib/Order/Partition/Finpartition.lean Outdated Show resolved Hide resolved

mathlib-triage bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Feb 10, 2026

yoh-tanimoto and others added 3 commits February 10, 2026 17:23

Update Mathlib/Order/Partition/Finpartition.lean

b1cecb9

Co-authored-by: Floris van Doorn <[email protected]>

Update Mathlib/Order/Partition/Finpartition.lean

5310245

Co-authored-by: Floris van Doorn <[email protected]>

Merge branch 'master' into variation-def

a2d6022

mathlib-bors bot changed the title ~~feat(MeasureTheory.VectorMeasure): add a definition of total variation for VectorMeasure~~ [Merged by Bors] - feat(MeasureTheory.VectorMeasure): add a definition of total variation for VectorMeasure Feb 10, 2026

mathlib-bors bot closed this Feb 10, 2026

yoh-tanimoto mentioned this pull request Mar 14, 2026

[Merged by Bors] - feat(Order/Partition/Finpartition): add toSubtype constructor #36489

Closed

2 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(MeasureTheory.VectorMeasure): add a definition of total variation for VectorMeasure#26156

[Merged by Bors] - feat(MeasureTheory.VectorMeasure): add a definition of total variation for VectorMeasure#26156
oliver-butterley wants to merge 149 commits intoleanprover-community:masterfrom
oliver-butterley:variation-def

oliver-butterley commented Jun 19, 2025 •

edited

Loading

Uh oh!

oliver-butterley commented Feb 3, 2026

Uh oh!

sgouezel commented Feb 3, 2026

Uh oh!

yoh-tanimoto commented Feb 3, 2026

Uh oh!

sgouezel commented Feb 7, 2026

Uh oh!

yoh-tanimoto commented Feb 9, 2026

Uh oh!

fpvandoorn left a comment

Uh oh!

Uh oh!

Uh oh!

mathlib-bors bot commented Feb 10, 2026

Uh oh!

yoh-tanimoto commented Feb 10, 2026

Uh oh!

mathlib-bors bot commented Feb 10, 2026

Uh oh!

oliver-butterley commented Feb 10, 2026

Uh oh!

mathlib-bors bot commented Feb 10, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

8 participants

Conversation

oliver-butterley commented Jun 19, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

oliver-butterley commented Feb 3, 2026

Uh oh!

sgouezel commented Feb 3, 2026

Uh oh!

yoh-tanimoto commented Feb 3, 2026

Uh oh!

sgouezel commented Feb 7, 2026

Uh oh!

yoh-tanimoto commented Feb 9, 2026

Uh oh!

fpvandoorn left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

mathlib-bors bot commented Feb 10, 2026

Uh oh!

yoh-tanimoto commented Feb 10, 2026

Uh oh!

mathlib-bors bot commented Feb 10, 2026

Uh oh!

oliver-butterley commented Feb 10, 2026

Uh oh!

mathlib-bors bot commented Feb 10, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

8 participants

oliver-butterley commented Jun 19, 2025 •

edited

Loading