# Mutually singular measures #

Two measures μ, ν are said to be mutually singular (MeasureTheory.Measure.MutuallySingular, 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 MeasureTheory.Measure.MutuallySingular.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 MeasureTheory.Measure.MutuallySingular and prove basic facts about it.

## Tags #

measure, mutually singular

def MeasureTheory.Measure.MutuallySingular {α : Type u_1} :
{x : } →

Two measures μ, ν are said to be mutually singular if there exists a measurable set s such that μ s = 0 and ν sᶜ = 0.

Equations
Instances For

Two measures μ, ν are said to be mutually singular if there exists a measurable set s such that μ s = 0 and ν sᶜ = 0.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem MeasureTheory.Measure.MutuallySingular.mk {α : Type u_1} {m0 : } {μ : } {ν : } {s : Set α} {t : Set α} (hs : μ s = 0) (ht : ν t = 0) (hst : Set.univ s t) :
def MeasureTheory.Measure.MutuallySingular.nullSet {α : Type u_1} {m0 : } {μ : } {ν : } :
Set α

A set such that μ h.nullSet = 0 and ν h.nullSetᶜ = 0.

Equations
Instances For
@[simp]
theorem MeasureTheory.Measure.MutuallySingular.measure_nullSet {α : Type u_1} {m0 : } {μ : } {ν : } :
@[simp]
theorem MeasureTheory.Measure.MutuallySingular.measure_compl_nullSet {α : Type u_1} {m0 : } {μ : } {ν : } :
@[simp]
theorem MeasureTheory.Measure.MutuallySingular.restrict_nullSet {α : Type u_1} {m0 : } {μ : } {ν : } :
μ.restrict = 0
@[simp]
theorem MeasureTheory.Measure.MutuallySingular.restrict_compl_nullSet {α : Type u_1} {m0 : } {μ : } {ν : } :
ν.restrict = 0
@[simp]
theorem MeasureTheory.Measure.MutuallySingular.zero_right {α : Type u_1} {m0 : } {μ : } :
theorem MeasureTheory.Measure.MutuallySingular.symm {α : Type u_1} {m0 : } {μ : } {ν : } :
theorem MeasureTheory.Measure.MutuallySingular.comm {α : Type u_1} {m0 : } {μ : } {ν : } :
@[simp]
theorem MeasureTheory.Measure.MutuallySingular.zero_left {α : Type u_1} {m0 : } {μ : } :
theorem MeasureTheory.Measure.MutuallySingular.mono_ac {α : Type u_1} {m0 : } {μ₁ : } {μ₂ : } {ν₁ : } {ν₂ : } (h : ) (hμ : ) (hν : ) :
theorem MeasureTheory.Measure.MutuallySingular.mono {α : Type u_1} {m0 : } {μ₁ : } {μ₂ : } {ν₁ : } {ν₂ : } (h : ) (hμ : μ₂ μ₁) (hν : ν₂ ν₁) :
@[simp]
theorem MeasureTheory.Measure.MutuallySingular.self_iff {α : Type u_1} {m0 : } (μ : ) :
@[simp]
theorem MeasureTheory.Measure.MutuallySingular.sum_left {α : Type u_1} {m0 : } {ν : } {ι : Type u_2} [] {μ : } :
∀ (i : ι),
@[simp]
theorem MeasureTheory.Measure.MutuallySingular.sum_right {α : Type u_1} {m0 : } {μ : } {ι : Type u_2} [] {ν : } :
∀ (i : ι),
@[simp]
theorem MeasureTheory.Measure.MutuallySingular.add_left_iff {α : Type u_1} {m0 : } {μ₁ : } {μ₂ : } {ν : } :
@[simp]
theorem MeasureTheory.Measure.MutuallySingular.add_right_iff {α : Type u_1} {m0 : } {μ : } {ν₁ : } {ν₂ : } :
theorem MeasureTheory.Measure.MutuallySingular.add_left {α : Type u_1} {m0 : } {μ : } {ν₁ : } {ν₂ : } (h₁ : ) (h₂ : ) :
theorem MeasureTheory.Measure.MutuallySingular.add_right {α : Type u_1} {m0 : } {μ : } {ν₁ : } {ν₂ : } (h₁ : ) (h₂ : ) :
theorem MeasureTheory.Measure.MutuallySingular.smul {α : Type u_1} {m0 : } {μ : } {ν : } (r : ENNReal) :
theorem MeasureTheory.Measure.MutuallySingular.smul_nnreal {α : Type u_1} {m0 : } {μ : } {ν : } (r : NNReal) :
theorem MeasureTheory.Measure.MutuallySingular.restrict {α : Type u_1} {m0 : } {μ : } {ν : } (s : Set α) :
theorem MeasureTheory.Measure.eq_zero_of_absolutelyContinuous_of_mutuallySingular {α : Type u_1} {m0 : } {μ : } {ν : } (h_ac : ) (h_ms : ) :
μ = 0