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 (μ - ν) + ν = μ.
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
- MeasureTheory.Measure.instSub = { sub := fun (μ ν : MeasureTheory.Measure α) => sInf {τ : MeasureTheory.Measure α | μ ≤ τ + ν} }
This application lemma only works in special circumstances. Given knowledge of
when μ ≤ ν and ν ≤ μ, a more general application lemma can be written.
Equations
- ⋯ = ⋯