Splitting a measure along a finite partition

A measure is the sum of its restrictions to the pieces of a finite almost-everywhere partition. Scaling each restriction by a factor s i ≤ 1 splits it further into a scaled part and a remainder, which is the form in which mass is matched cell by cell in transport-plan constructions.

Main statements

• MeasureTheory.Measure.eq_sum_smul_restrict_add_sum_one_sub_smul_restrict — for a finite family A of null-measurable, pairwise a.e.-disjoint sets covering almost everything, and factors s i ≤ 1, μ = ∑ i, s i • μ.restrict (A i) + ∑ i, (1 - s i) • μ.restrict (A i).

theorem MeasureTheory.Measure.eq_sum_smul_restrict_add_sum_one_sub_smul_restrict {Z : Type u_1} [MeasurableSpace Z] {μ : Measure Z} {ι : Type u_2} [Fintype ι] {A : ι → Set Z} (hAm : ∀ (i : ι), NullMeasurableSet (A i) μ) (hAd : Pairwise (Function.onFun (AEDisjoint μ) A)) (hAu : ⋃ (i : ι), A i =ᵐ[μ] Set.univ) {s : ι → ENNReal} (hs : ∀ (i : ι), s i ≤ 1) : μ = ∑ i : ι, s i • μ.restrict (A i) + ∑ i : ι, (1 - s i) • μ.restrict (A i)

Splitting each piece of a finite almost-everywhere partition by a factor s i ≤ 1 splits the measure into a scaled part and a remainder.