# mathlib3documentation

measure_theory.measure.mutually_singular

# Mutually singular measures #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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.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 ι] {μ : ι } :
(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 ι] {ν : ι } :
(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 ν
@[simp]
theorem measure_theory.measure.mutually_singular.add_right_iff {α : Type u_1} {m0 : measurable_space α} {μ ν₁ ν₂ : measure_theory.measure α} :
μ.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 (ν₁ + ν₂)