# Documentation

Mathlib.MeasureTheory.Measure.MutuallySingular

# 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.

Instances For

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

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) :
@[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.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) :