Subtraction of measures #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.has_sub.
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.has_sub.
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
- measure_theory.measure.has_sub = {sub := λ (μ ν : measure_theory.measure α), has_Inf.Inf {τ : measure_theory.measure α | μ ≤ τ + ν}}
This application lemma only works in special circumstances. Given knowledge of
when μ ≤ ν and ν ≤ μ, a more general application lemma can be written.