# 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

source
def MeasureTheory.Measure.MutuallySingular {α : Type u_1} {x✝ : MeasurableSpace α} (μ ν : 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

- μ.MutuallySingular ν = ∃ (s : Set α), MeasurableSet s ∧ μ s = 0 ∧ ν s ᶜ = 0

Instances For

source
def MeasureTheory.«term_⟂ₘ_» :
Lean.TrailingParserDescr

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

Equations

- MeasureTheory.«term_⟂ₘ_» = Lean.ParserDescr.trailingNode `MeasureTheory.«term_⟂ₘ_» 60 60 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⟂ₘ ") (Lean.ParserDescr.cat `term 61))

Instances For

source
theorem MeasureTheory.Measure.MutuallySingular.mk {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} {s t : Set α} (hs : μ s = 0) (ht : ν t = 0) (hst : Set.univ ⊆ s ∪ t) :
μ.MutuallySingular ν
source
def MeasureTheory.Measure.MutuallySingular.nullSet {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} (h : μ.MutuallySingular ν) :
Set α

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

Equations

- h.nullSet = Exists.choose h

Instances For

source
theorem MeasureTheory.Measure.MutuallySingular.measurableSet_nullSet {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} (h : μ.MutuallySingular ν) :
MeasurableSet h.nullSet
source
@[simp]
theorem MeasureTheory.Measure.MutuallySingular.measure_nullSet {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} (h : μ.MutuallySingular ν) :
μ h.nullSet = 0
source
@[simp]
theorem MeasureTheory.Measure.MutuallySingular.measure_compl_nullSet {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} (h : μ.MutuallySingular ν) :
ν h.nullSet ᶜ = 0
source
@[simp]
theorem MeasureTheory.Measure.MutuallySingular.restrict_nullSet {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} (h : μ.MutuallySingular ν) :
μ.restrict h.nullSet = 0
source
@[simp]
theorem MeasureTheory.Measure.MutuallySingular.restrict_compl_nullSet {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} (h : μ.MutuallySingular ν) :
ν.restrict h.nullSet ᶜ = 0
source
@[simp]
theorem MeasureTheory.Measure.MutuallySingular.zero_right {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} :
μ.MutuallySingular 0
source
theorem MeasureTheory.Measure.MutuallySingular.symm {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} (h : ν.MutuallySingular μ) :
μ.MutuallySingular ν
source
theorem MeasureTheory.Measure.MutuallySingular.comm {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} :
μ.MutuallySingular ν ↔ ν.MutuallySingular μ
source
@[simp]
theorem MeasureTheory.Measure.MutuallySingular.zero_left {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} :
MutuallySingular 0 μ
source
theorem MeasureTheory.Measure.MutuallySingular.mono_ac {α : Type u_1} {m0 : MeasurableSpace α} {μ₁ μ₂ ν₁ ν₂ : Measure α} (h : μ₁.MutuallySingular ν₁) (hμ : μ₂.AbsolutelyContinuous μ₁) (hν : ν₂.AbsolutelyContinuous ν₁) :
μ₂.MutuallySingular ν₂
source
theorem MeasureTheory.Measure.MutuallySingular.congr_ac {α : Type u_1} {m0 : MeasurableSpace α} {μ μ₂ ν ν₂ : Measure α} (hμμ₂ : μ.AbsolutelyContinuous μ₂) (hμ₂μ : μ₂.AbsolutelyContinuous μ) (hνν₂ : ν.AbsolutelyContinuous ν₂) (hν₂ν : ν₂.AbsolutelyContinuous ν) :
μ.MutuallySingular ν ↔ μ₂.MutuallySingular ν₂
source
theorem MeasureTheory.Measure.MutuallySingular.mono {α : Type u_1} {m0 : MeasurableSpace α} {μ₁ μ₂ ν₁ ν₂ : Measure α} (h : μ₁.MutuallySingular ν₁) (hμ : μ₂ ≤ μ₁) (hν : ν₂ ≤ ν₁) :
μ₂.MutuallySingular ν₂
source
@[simp]
theorem MeasureTheory.Measure.MutuallySingular.self_iff {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) :
μ.MutuallySingular μ ↔ μ = 0
source
@[simp]
theorem MeasureTheory.Measure.MutuallySingular.sum_left {α : Type u_1} {m0 : MeasurableSpace α} {ν : Measure α} {ι : Type u_2} [Countable ι] {μ : ι → Measure α} :
(sum μ).MutuallySingular ν ↔ ∀ (i : ι), (μ i).MutuallySingular ν
source
@[simp]
theorem MeasureTheory.Measure.MutuallySingular.sum_right {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {ι : Type u_2} [Countable ι] {ν : ι → Measure α} :
μ.MutuallySingular (sum ν) ↔ ∀ (i : ι), μ.MutuallySingular (ν i)
source
@[simp]
theorem MeasureTheory.Measure.MutuallySingular.add_left_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ₁ μ₂ ν : Measure α} :
(μ₁ + μ₂).MutuallySingular ν ↔ μ₁.MutuallySingular ν ∧ μ₂.MutuallySingular ν
source
@[simp]
theorem MeasureTheory.Measure.MutuallySingular.add_right_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ ν₁ ν₂ : Measure α} :
μ.MutuallySingular (ν₁ + ν₂) ↔ μ.MutuallySingular ν₁ ∧ μ.MutuallySingular ν₂
source
theorem MeasureTheory.Measure.MutuallySingular.add_left {α : Type u_1} {m0 : MeasurableSpace α} {μ ν₁ ν₂ : Measure α} (h₁ : ν₁.MutuallySingular μ) (h₂ : ν₂.MutuallySingular μ) :
(ν₁ + ν₂).MutuallySingular μ
source
theorem MeasureTheory.Measure.MutuallySingular.add_right {α : Type u_1} {m0 : MeasurableSpace α} {μ ν₁ ν₂ : Measure α} (h₁ : μ.MutuallySingular ν₁) (h₂ : μ.MutuallySingular ν₂) :
μ.MutuallySingular (ν₁ + ν₂)
source
theorem MeasureTheory.Measure.MutuallySingular.smul {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} (r : ENNReal) (h : ν.MutuallySingular μ) :
(r • ν).MutuallySingular μ
source
theorem MeasureTheory.Measure.MutuallySingular.smul_nnreal {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} (r : NNReal) (h : ν.MutuallySingular μ) :
(r • ν).MutuallySingular μ
source
theorem MeasureTheory.Measure.MutuallySingular.restrict {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} (h : μ.MutuallySingular ν) (s : Set α) :
(μ.restrict s).MutuallySingular ν
source
theorem MeasureTheory.Measure.eq_zero_of_absolutelyContinuous_of_mutuallySingular {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} (h_ac : μ.AbsolutelyContinuous ν) (h_ms : μ.MutuallySingular ν) :
μ = 0
source
theorem MeasureTheory.Measure.absolutelyContinuous_of_add_of_mutuallySingular {α : Type u_1} {m0 : MeasurableSpace α} {μ ν₁ ν₂ : Measure α} (h : μ.AbsolutelyContinuous (ν₁ + ν₂)) (h_ms : μ.MutuallySingular ν₂) :
μ.AbsolutelyContinuous ν₁
source
theorem MeasurableEmbedding.mutuallySingular_map {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {β : Type u_2} {x✝ : MeasurableSpace β} {f : α → β} (hf : MeasurableEmbedding f) (hμν : μ.MutuallySingular ν) :
(MeasureTheory.Measure.map f μ).MutuallySingular (MeasureTheory.Measure.map f ν)
source
theorem MeasureTheory.Measure.exists_null_set_measure_lt_of_disjoint {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} (h : Disjoint μ ν) {ε : NNReal} (hε : 0 < ε) :
∃ (s : Set α), μ s = 0 ∧ ν s ᶜ ≤ 2 * ↑ε
source
theorem MeasureTheory.Measure.mutuallySingular_of_disjoint {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} (h : Disjoint μ ν) :
μ.MutuallySingular ν
source
theorem MeasureTheory.Measure.MutuallySingular.disjoint {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} (h : μ.MutuallySingular ν) :
Disjoint μ ν
source
theorem MeasureTheory.Measure.MutuallySingular.disjoint_ae {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} (h : μ.MutuallySingular ν) :
Disjoint (ae μ) (ae ν)
source
theorem MeasureTheory.Measure.disjoint_of_disjoint_ae {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} (h : Disjoint (ae μ) (ae ν)) :
Disjoint μ ν
source
theorem MeasureTheory.Measure.mutuallySingular_tfae {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} :
[μ.MutuallySingular ν, Disjoint μ ν, Disjoint (ae μ) (ae ν)].TFAE
source
theorem MeasureTheory.Measure.mutuallySingular_iff_disjoint {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} :
μ.MutuallySingular ν ↔ Disjoint μ ν
source
theorem MeasureTheory.Measure.mutuallySingular_iff_disjoint_ae {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} :
μ.MutuallySingular ν ↔ Disjoint (ae μ) (ae ν)