Mutually singular measures #
Two measures μ, ν are said to be mutually singular (measure_theory.measure.mutually_singular,
localized notation μ ⊥ₘ ν) if there exists a measurable set s such that μ s = 0 and
ν sᶜ = 0. The measurability of s is an unnecessary assumption (see
measure_theory.measure.mutually_singular.mk) but we keep it because this way rcases (h : μ ⊥ₘ ν)
gives us a measurable set and usually it is easy to prove measurability.
In this file we define the predicate measure_theory.measure.mutually_singular and prove basic
facts about it.
Tags #
measure, mutually singular
def
measure_theory.measure.mutually_singular
{α : Type u_1}
{m0 : measurable_space α}
(μ ν : measure_theory.measure α) :
Prop
Two measures μ, ν are said to be mutually singular if there exists a measurable set s
such that μ s = 0 and ν sᶜ = 0.
theorem
measure_theory.measure.mutually_singular.mk
{α : Type u_1}
{m0 : measurable_space α}
{μ ν : measure_theory.measure α}
{s t : set α}
(hs : ⇑μ s = 0)
(ht : ⇑ν t = 0)
(hst : set.univ ⊆ s ∪ t) :
@[simp]
theorem
measure_theory.measure.mutually_singular.zero_right
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α} :
@[symm]
theorem
measure_theory.measure.mutually_singular.symm
{α : Type u_1}
{m0 : measurable_space α}
{μ ν : measure_theory.measure α}
(h : ν.mutually_singular μ) :
theorem
measure_theory.measure.mutually_singular.comm
{α : Type u_1}
{m0 : measurable_space α}
{μ ν : measure_theory.measure α} :
μ.mutually_singular ν ↔ ν.mutually_singular μ
@[simp]
theorem
measure_theory.measure.mutually_singular.zero_left
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α} :
theorem
measure_theory.measure.mutually_singular.mono_ac
{α : Type u_1}
{m0 : measurable_space α}
{μ₁ μ₂ ν₁ ν₂ : measure_theory.measure α}
(h : μ₁.mutually_singular ν₁)
(hμ : μ₂.absolutely_continuous μ₁)
(hν : ν₂.absolutely_continuous ν₁) :
μ₂.mutually_singular ν₂
theorem
measure_theory.measure.mutually_singular.mono
{α : Type u_1}
{m0 : measurable_space α}
{μ₁ μ₂ ν₁ ν₂ : measure_theory.measure α}
(h : μ₁.mutually_singular ν₁)
(hμ : μ₂ ≤ μ₁)
(hν : ν₂ ≤ ν₁) :
μ₂.mutually_singular ν₂
@[simp]
theorem
measure_theory.measure.mutually_singular.sum_left
{α : Type u_1}
{m0 : measurable_space α}
{ν : measure_theory.measure α}
{ι : Type u_2}
[countable ι]
{μ : ι → measure_theory.measure α} :
(measure_theory.measure.sum μ).mutually_singular ν ↔ ∀ (i : ι), (μ i).mutually_singular ν
@[simp]
theorem
measure_theory.measure.mutually_singular.sum_right
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{ι : Type u_2}
[countable ι]
{ν : ι → measure_theory.measure α} :
μ.mutually_singular (measure_theory.measure.sum ν) ↔ ∀ (i : ι), μ.mutually_singular (ν i)
@[simp]
theorem
measure_theory.measure.mutually_singular.add_left_iff
{α : Type u_1}
{m0 : measurable_space α}
{μ₁ μ₂ ν : measure_theory.measure α} :
(μ₁ + μ₂).mutually_singular ν ↔ μ₁.mutually_singular ν ∧ μ₂.mutually_singular ν
@[simp]
theorem
measure_theory.measure.mutually_singular.add_right_iff
{α : Type u_1}
{m0 : measurable_space α}
{μ ν₁ ν₂ : measure_theory.measure α} :
μ.mutually_singular (ν₁ + ν₂) ↔ μ.mutually_singular ν₁ ∧ μ.mutually_singular ν₂
theorem
measure_theory.measure.mutually_singular.add_left
{α : Type u_1}
{m0 : measurable_space α}
{μ ν₁ ν₂ : measure_theory.measure α}
(h₁ : ν₁.mutually_singular μ)
(h₂ : ν₂.mutually_singular μ) :
(ν₁ + ν₂).mutually_singular μ
theorem
measure_theory.measure.mutually_singular.add_right
{α : Type u_1}
{m0 : measurable_space α}
{μ ν₁ ν₂ : measure_theory.measure α}
(h₁ : μ.mutually_singular ν₁)
(h₂ : μ.mutually_singular ν₂) :
μ.mutually_singular (ν₁ + ν₂)
theorem
measure_theory.measure.mutually_singular.smul
{α : Type u_1}
{m0 : measurable_space α}
{μ ν : measure_theory.measure α}
(r : ennreal)
(h : ν.mutually_singular μ) :
(r • ν).mutually_singular μ
theorem
measure_theory.measure.mutually_singular.smul_nnreal
{α : Type u_1}
{m0 : measurable_space α}
{μ ν : measure_theory.measure α}
(r : nnreal)
(h : ν.mutually_singular μ) :
(r • ν).mutually_singular μ