Stieltjes vector measures #34055

Stream: PR reviews

[Sébastien Gouëzel]

In #PNT, integration by parts wrt bounded variation functions is a stumbling block. So, as a first step, I had a go at defining the vector measure associated to a bounded variation function. As always, this was more complicated than expected (because all our beautiful theorems to construct measures rely crucially on the order, and therefore don't apply to construct vector measures in a general vector space -- one could take shortcuts for signed measures, but I went for the general version instead). Done in #34055, but with +2160/-146 so it will take some time to get this into Mathlib. I split the first few prerequisites, which are all essentially trivial but I'm mentioning here for the record:

[Sébastien Gouëzel]

#34410 (+37/-4): lemmas about symmDiff and finite sums

[Sébastien Gouëzel]

#34411 (+27/-1): missing basic analysis and topology API

[Sébastien Gouëzel]

#34413 (+22/-8): add atBot version of convergence lemmas, rename original lemma for disambiguation

[Sébastien Gouëzel]

#34414 (+85/-2): more basic API on vector measures

[Sébastien Gouëzel]

#34434 (+103/-92, but just moving things around): let AddContent take values in a general monoid

[Ruben Van de Velde]

Sébastien Gouëzel said:

#34110 (+37/-4): lemmas about symmDiff and finite sums

#34410

[Sébastien Gouëzel]

#34437 (+40/-0): open-closed intervals form a semiring of sets

[Sébastien Gouëzel]

#34438 (+28/-0): the extension of a Lipschitz function is Lipschitz

[Sébastien Gouëzel]

#34412 (+175/-11): more on left and right limits

[Sébastien Gouëzel]

#34462 (+129/-0): additive content on open-closed intervals, mapping (u, v] to f v - f u.

[Sébastien Gouëzel]

#34499 (+152/-0): an additive content on a semiring of sets extends to the generated ring of sets

[Sébastien Gouëzel]

#34517 (+186/-0): distance on the set of measurable sets given by the measure of the symmetric difference

[Sébastien Gouëzel]

#34415 (+52/-17): improve Stieltjes measure file

[Sébastien Gouëzel]

#34559 (+476/-14): bounded variation functions have left and right limits, and limits at infinity
That's a long one, unfortunately. Everything in the PR is on the same topic, which is why I have kept it as a single PR. I can split it into two parts if it's too long, though, just tell me!

[Sébastien Gouëzel]

#34654 (+292/-0): extend an additive content to a vector measure under a domination condition

[Sébastien Gouëzel]

In fact I think I can improve the statement of this one, so don't review yet please.

[Sébastien Gouëzel]

#34680 (+45/-0): measurable union of a family of measurable sets

[Sébastien Gouëzel]

#34654 (+320/-0): extend an additive content to a vector measure under a domination condition
is now ready, with an improved statement compared to the previous version (an assumption has been dropped).

[Sébastien Gouëzel]

Thanks to the heroic efforts of the reviewers, we are almost there: there is a single PR left giving the main construction
#34055 (+272/-0): vector measures associated to functions of bounded variation