Partial sums of the measures of a disjoint family

For a family f of null-measurable sets that are pairwise almost everywhere disjoint, the mass of any finite subfamily is bounded by the mass of the union. When the union has finite mass, the mass of the union not yet covered by the first n sets tends to zero.

Main results

• MeasureTheory.sum_measure_le_measure_iUnion: ∑ i ∈ s, μ (f i) ≤ μ (⋃ i, f i).
• MeasureTheory.tendsto_measure_iUnion_sub_sum_range: μ (⋃ k, f k) - ∑ k ∈ range n, μ (f k) → 0 as n → ∞, if μ (⋃ k, f k) ≠ ∞.
• MeasureTheory.measure_le_mul_measure_biUnion: if almost all of A is covered by a countable a.e. disjoint family of sets, each meeting A in at most a δ fraction of its measure, then μ A ≤ δ μ (⋃ i ∈ s, f i).

theorem MeasureTheory.sum_measure_le_measure_iUnion {α : Type u_1} {ι : Type u_2} {mα : MeasurableSpace α} {μ : Measure α} {f : ι → Set α} (hf : ∀ (i : ι), NullMeasurableSet (f i) μ) (hdisj : Pairwise (Function.onFun (AEDisjoint μ) f)) (s : Finset ι) : ∑ i ∈ s, μ (f i) ≤ μ (⋃ (i : ι), f i)

The measures of the sets in a finite subfamily of a pairwise a.e. disjoint family of null-measurable sets add up to at most the measure of the union of the whole family.

theorem MeasureTheory.tendsto_measure_iUnion_sub_sum_range {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} {f : ℕ → Set α} (hf : ∀ (k : ℕ), NullMeasurableSet (f k) μ) (hdisj : Pairwise (Function.onFun (AEDisjoint μ) f)) (hfin : μ (⋃ (k : ℕ), f k) ≠ ⊤) : Filter.Tendsto (fun (n : ℕ) => μ (⋃ (k : ℕ), f k) - ∑ k ∈ Finset.range n, μ (f k)) Filter.atTop (nhds 0)

For a pairwise a.e. disjoint sequence of null-measurable sets whose union has finite measure, the part of the union's measure not covered by the first n sets tends to zero.

theorem MeasureTheory.measure_le_mul_measure_biUnion {α : Type u_1} {ι : Type u_2} {mα : MeasurableSpace α} {μ : Measure α} {f : ι → Set α} {s : Set ι} {A : Set α} {δ : ENNReal} (hs : s.Countable) (hf : ∀ i ∈ s, NullMeasurableSet (f i) μ) (hdisj : s.Pairwise (Function.onFun (AEDisjoint μ) f)) (hA : μ (A \ ⋃ i ∈ s, f i) = 0) (hδ : ∀ i ∈ s, μ (A ∩ f i) ≤ δ * μ (f i)) : μ A ≤ δ * μ (⋃ i ∈ s, f i)

If almost all of A is covered by a countable pairwise a.e. disjoint family of null-measurable sets f i, i ∈ s, each meeting A in at most a δ fraction of its measure, then the measure of A is at most δ times the measure of their union.