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) :
μ ⊥ₘ ν
theorem measure_theory.measure.mutually_singular.symm {α : Type u_1} {m0 : measurable_space α} {μ ν : measure_theory.measure α} (h : ν ⊥ₘ μ) :
μ ⊥ₘ ν
theorem measure_theory.measure.mutually_singular.comm {α : 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 : μ₁ ⊥ₘ ν₁) (hμ : μ₂ μ₁) (hν : ν₂ ν₁) :
μ₂ ⊥ₘ ν₂
theorem measure_theory.measure.mutually_singular.mono {α : Type u_1} {m0 : measurable_space α} {μ₁ μ₂ ν₁ ν₂ : measure_theory.measure α} (h : μ₁ ⊥ₘ ν₁) (hμ : μ₂ μ₁) (hν : ν₂ ν₁) :
μ₂ ⊥ₘ ν₂
@[simp]
theorem measure_theory.measure.mutually_singular.sum_left {α : Type u_1} {m0 : measurable_space α} {ν : measure_theory.measure α} {ι : Type u_2} [encodable ι] {μ : ι → measure_theory.measure α} :
measure_theory.measure.sum μ ⊥ₘ ν ∀ (i : ι), μ i ⊥ₘ ν
@[simp]
theorem measure_theory.measure.mutually_singular.sum_right {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {ι : Type u_2} [encodable ι] {ν : ι → measure_theory.measure α} :
μ ⊥ₘ measure_theory.measure.sum ν ∀ (i : ι), μ ⊥ₘ ν i
@[simp]
theorem measure_theory.measure.mutually_singular.add_left_iff {α : Type u_1} {m0 : measurable_space α} {μ₁ μ₂ ν : measure_theory.measure α} :
μ₁ + μ₂ ⊥ₘ ν μ₁ ⊥ₘ ν μ₂ ⊥ₘ ν
@[simp]
theorem measure_theory.measure.mutually_singular.add_right_iff {α : Type u_1} {m0 : measurable_space α} {μ ν₁ ν₂ : measure_theory.measure α} :
μ ⊥ₘ ν₁ + ν₂ μ ⊥ₘ ν₁ μ ⊥ₘ ν₂
theorem measure_theory.measure.mutually_singular.add_left {α : Type u_1} {m0 : measurable_space α} {μ ν₁ ν₂ : measure_theory.measure α} (h₁ : ν₁ ⊥ₘ μ) (h₂ : ν₂ ⊥ₘ μ) :
ν₁ + ν₂ ⊥ₘ μ
theorem measure_theory.measure.mutually_singular.add_right {α : Type u_1} {m0 : measurable_space α} {μ ν₁ ν₂ : measure_theory.measure α} (h₁ : μ ⊥ₘ ν₁) (h₂ : μ ⊥ₘ ν₂) :
μ ⊥ₘ ν₁ + ν₂
theorem measure_theory.measure.mutually_singular.smul {α : Type u_1} {m0 : measurable_space α} {μ ν : measure_theory.measure α} (r : ℝ≥0∞) (h : ν ⊥ₘ μ) :
r ν ⊥ₘ μ
theorem measure_theory.measure.mutually_singular.smul_nnreal {α : Type u_1} {m0 : measurable_space α} {μ ν : measure_theory.measure α} (r : ℝ≥0) (h : ν ⊥ₘ μ) :
r ν ⊥ₘ μ