Results about subtraction of finite measures

The content of this file is not placed in MeasureTheory.Measure.Sub because it uses tools that are not imported in the other file: the Hahn decomposition of finite measures and measures built with withDensity.

Main statements

• sub_le_iff_le_add: for μ and ν finite measures, μ - ν ≤ ξ ↔ μ ≤ ξ + ν. See also sub_le_iff_le_add_of_le for the case where only ν is finite, with the additional hypothesis ν ≤ μ.
• withDensity_sub: If μ.withDensity g is finite, then μ.withDensity (f - g) = μ.withDensity f - μ.withDensity g.

theorem MeasureTheory.Measure.sub_le_iff_le_add {α : Type u_1} {mα : MeasurableSpace α} {μ ν ξ : Measure α} [IsFiniteMeasure μ] [IsFiniteMeasure ν] : μ - ν ≤ ξ ↔ μ ≤ ξ + ν

theorem MeasureTheory.Measure.withDensity_sub_of_le {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} {f g : α → ENNReal} [IsFiniteMeasure (μ.withDensity g)] (hg : Measurable g) (hgf : g ≤ᵐ[μ] f) : μ.withDensity (f - g) = μ.withDensity f - μ.withDensity g

theorem MeasureTheory.Measure.withDensity_sub {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} {f g : α → ENNReal} [IsFiniteMeasure (μ.withDensity g)] (hf : Measurable f) (hg : Measurable g) : μ.withDensity (f - g) = μ.withDensity f - μ.withDensity g