Estimates in symmetric-difference outer measure

For sets of finite outer measure, the mass of a set changes by at most the mass of its symmetric difference with another set. The intersection estimate follows by containing its symmetric difference in the union of the two input symmetric differences.

These statements use only monotonicity and subadditivity, so they are stated for OuterMeasureClass, which covers both outer measures and measures without requiring a measurable space. They supply the approximation estimates for the Hewitt–Savage zero-one criterion in TauCeti/MeasureTheory/Measure/ZeroOne.lean.

Main results

• TauCeti.MeasureTheory.abs_toReal_sub_le_toReal_symmDiff
• TauCeti.MeasureTheory.abs_toReal_inter_sub_le_toReal_symmDiff_add

theorem TauCeti.MeasureTheory.abs_toReal_sub_le_toReal_symmDiff {Ω : Type u_1} {F : Type u_2} [FunLike F (Set Ω) ENNReal] [MeasureTheory.OuterMeasureClass F Ω] {μ : F} {s t : Set Ω} (hs : μ s ≠ ⊤) (ht : μ t ≠ ⊤) : |(μ s).toReal - (μ t).toReal| ≤ (μ (symmDiff s t)).toReal

For sets of finite outer measure, the difference of their masses is bounded by the mass of their symmetric difference. No measurability or additivity is needed.

This generalizes Mathlib's MeasureTheory.abs_measureReal_sub_le_measureReal_symmDiff' and its finite-measure wrapper MeasureTheory.abs_measureReal_sub_le_measureReal_symmDiff.

theorem TauCeti.MeasureTheory.abs_toReal_inter_sub_le_toReal_symmDiff_add {Ω : Type u_1} {F : Type u_2} [FunLike F (Set Ω) ENNReal] [MeasureTheory.OuterMeasureClass F Ω] {μ : F} {A B s : Set Ω} (hs : μ s ≠ ⊤) (hA : μ (symmDiff A s) ≠ ⊤) (hB : μ (symmDiff B s) ≠ ⊤) : |(μ (A ∩ B)).toReal - (μ s).toReal| ≤ (μ (symmDiff A s)).toReal + (μ (symmDiff B s)).toReal

If s and the two symmetric differences have finite outer measure, the mass of A ∩ B is within their summed symmetric-difference masses of the mass of s.