mathlib documentation

measure_theory.measure.mutually_singular

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.

Equations
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) :
@[symm]
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 α} :
@[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 α} :
@[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 (ν₁ + ν₂)