mathlib documentation

measure_theory.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.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 (μ - ν) + ν = μ.

@[protected, instance]
noncomputable def measure_theory.measure.has_sub {α : Type u_1} [measurable_space α] :

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
theorem measure_theory.measure.sub_def {α : Type u_1} {m : measurable_space α} {μ ν : measure_theory.measure α} :
μ - ν = has_Inf.Inf {d : measure_theory.measure α | μ d + ν}
theorem measure_theory.measure.sub_le_of_le_add {α : Type u_1} {m : measurable_space α} {μ ν d : measure_theory.measure α} (h : μ d + ν) :
μ - ν d
theorem measure_theory.measure.sub_eq_zero_of_le {α : Type u_1} {m : measurable_space α} {μ ν : measure_theory.measure α} (h : μ ν) :
μ - ν = 0
theorem measure_theory.measure.sub_le {α : Type u_1} {m : measurable_space α} {μ ν : measure_theory.measure α} :
μ - ν μ
@[simp]
theorem measure_theory.measure.sub_top {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} :
μ - = 0
@[simp]
theorem measure_theory.measure.zero_sub {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} :
0 - μ = 0
@[simp]
theorem measure_theory.measure.sub_self {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} :
μ - μ = 0
theorem measure_theory.measure.sub_apply {α : Type u_1} {m : measurable_space α} {μ ν : measure_theory.measure α} {s : set α} [measure_theory.is_finite_measure ν] (h₁ : measurable_set 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.

theorem measure_theory.measure.sub_add_cancel_of_le {α : Type u_1} {m : measurable_space α} {μ ν : measure_theory.measure α} [measure_theory.is_finite_measure ν] (h₁ : ν μ) :
μ - ν + ν = μ
theorem measure_theory.measure.restrict_sub_eq_restrict_sub_restrict {α : Type u_1} {m : measurable_space α} {μ ν : measure_theory.measure α} {s : set α} (h_meas_s : measurable_set s) :
- ν).restrict s = μ.restrict s - ν.restrict s
theorem measure_theory.measure.sub_apply_eq_zero_of_restrict_le_restrict {α : Type u_1} {m : measurable_space α} {μ ν : measure_theory.measure α} {s : set α} (h_le : μ.restrict s ν.restrict s) (h_meas_s : measurable_set s) :
- ν) s = 0