Documentation

Mathlib.MeasureTheory.Measure.Sub

Subtraction of measures #

In this file we define μ - ν to be the least measure τ such that μ ≤ τ + ν. It is the equivalent of (μ - ν) ⊔ 0 if μ and ν were signed measures. Compare with ENNReal.instSub. Specifically, note that if you have α = {1,2}, and μ {1} = 2, μ {2} = 0, and ν {2} = 2, ν {1} = 0, then (μ - ν) {1, 2} = 2. However, if μ ≤ ν, and ν univ ≠ ∞, then (μ - ν) + ν = μ.

source
noncomputable instance MeasureTheory.Measure.instSub {α : Type u_1} [MeasurableSpace α] :
Sub (MeasureTheory.Measure α)

The measure μ - ν is defined to be the least measure τ such that μ ≤ τ + ν. It is the equivalent of (μ - ν) ⊔ 0 if μ and ν were signed measures. Compare with ENNReal.instSub. Specifically, note that if you have α = {1,2}, and μ {1} = 2, μ {2} = 0, and ν {2} = 2, ν {1} = 0, then (μ - ν) {1, 2} = 2. However, if μ ≤ ν, and ν univ ≠ ∞, then (μ - ν) + ν = μ.

Equations
source
theorem MeasureTheory.Measure.sub_def {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} :
μ - ν = sInf {d : MeasureTheory.Measure α | μ ≤ d + ν}
source
theorem MeasureTheory.Measure.sub_le_of_le_add {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {d : MeasureTheory.Measure α} (h : μ ≤ d + ν) :
μ - ν ≤ d
source
theorem MeasureTheory.Measure.sub_eq_zero_of_le {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (h : μ ≤ ν) :
μ - ν = 0
source
theorem MeasureTheory.Measure.sub_le {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} :
μ - ν ≤ μ
source
@[simp]
theorem MeasureTheory.Measure.sub_top {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} :
μ - ⊤ = 0
source
@[simp]
theorem MeasureTheory.Measure.zero_sub {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} :
0 - μ = 0
source
@[simp]
theorem MeasureTheory.Measure.sub_self {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} :
μ - μ = 0
source
theorem MeasureTheory.Measure.sub_apply {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsFiniteMeasure ν] (h₁ : MeasurableSet s) (h₂ : ν ≤ μ) :
↑↑(μ - ν) s = ↑↑μ s - ↑↑ν s

This application lemma only works in special circumstances. Given knowledge of when μ ≤ ν and ν ≤ μ, a more general application lemma can be written.

source
theorem MeasureTheory.Measure.sub_add_cancel_of_le {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure ν] (h₁ : ν ≤ μ) :
μ - ν + ν = μ
source
theorem MeasureTheory.Measure.restrict_sub_eq_restrict_sub_restrict {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {s : Set α} (h_meas_s : MeasurableSet s) :
MeasureTheory.Measure.restrict (μ - ν) s = MeasureTheory.Measure.restrict μ s - MeasureTheory.Measure.restrict ν s
source
theorem MeasureTheory.Measure.sub_apply_eq_zero_of_restrict_le_restrict {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {s : Set α} (h_le : MeasureTheory.Measure.restrict μ s ≤ MeasureTheory.Measure.restrict ν s) (h_meas_s : MeasurableSet s) :
↑↑(μ - ν) s = 0
source
instance MeasureTheory.Measure.isFiniteMeasure_sub {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] :
MeasureTheory.IsFiniteMeasure (μ - ν)
Equations