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✝ : 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

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))

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 ν

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

theorem MeasureTheory.Measure.MutuallySingular.measurableSet_nullSet {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} (h : μ.MutuallySingular ν) : MeasurableSet h.nullSet

@[simp]

theorem MeasureTheory.Measure.MutuallySingular.measure_nullSet {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} (h : μ.MutuallySingular ν) : μ h.nullSet = 0

@[simp]

theorem MeasureTheory.Measure.MutuallySingular.measure_compl_nullSet {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} (h : μ.MutuallySingular ν) : ν h.nullSetᶜ = 0

@[simp]

theorem MeasureTheory.Measure.MutuallySingular.restrict_nullSet {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} (h : μ.MutuallySingular ν) : μ.restrict h.nullSet = 0

@[simp]

theorem MeasureTheory.Measure.MutuallySingular.restrict_compl_nullSet {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} (h : μ.MutuallySingular ν) : ν.restrict h.nullSetᶜ = 0

@[simp]

theorem MeasureTheory.Measure.MutuallySingular.zero_right {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} : μ.MutuallySingular 0

theorem MeasureTheory.Measure.MutuallySingular.symm {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} (h : ν.MutuallySingular μ) : μ.MutuallySingular ν

theorem MeasureTheory.Measure.MutuallySingular.comm {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} : μ.MutuallySingular ν ↔ ν.MutuallySingular μ

@[simp]

theorem MeasureTheory.Measure.MutuallySingular.zero_left {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} : MutuallySingular 0 μ

theorem MeasureTheory.Measure.MutuallySingular.mono_ac {α : Type u_1} {m0 : MeasurableSpace α} {μ₁ μ₂ ν₁ ν₂ : Measure α} (h : μ₁.MutuallySingular ν₁) (hμ : μ₂.AbsolutelyContinuous μ₁) (hν : ν₂.AbsolutelyContinuous ν₁) : μ₂.MutuallySingular ν₂

theorem MeasureTheory.Measure.MutuallySingular.congr_ac {α : Type u_1} {m0 : MeasurableSpace α} {μ μ₂ ν ν₂ : Measure α} (hμμ₂ : μ.AbsolutelyContinuous μ₂) (hμ₂μ : μ₂.AbsolutelyContinuous μ) (hνν₂ : ν.AbsolutelyContinuous ν₂) (hν₂ν : ν₂.AbsolutelyContinuous ν) : μ.MutuallySingular ν ↔ μ₂.MutuallySingular ν₂

theorem MeasureTheory.Measure.MutuallySingular.mono {α : Type u_1} {m0 : MeasurableSpace α} {μ₁ μ₂ ν₁ ν₂ : Measure α} (h : μ₁.MutuallySingular ν₁) (hμ : μ₂ ≤ μ₁) (hν : ν₂ ≤ ν₁) : μ₂.MutuallySingular ν₂

@[simp]

theorem MeasureTheory.Measure.MutuallySingular.self_iff {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) : μ.MutuallySingular μ ↔ μ = 0

@[simp]

theorem MeasureTheory.Measure.MutuallySingular.sum_left {α : Type u_1} {m0 : MeasurableSpace α} {ν : Measure α} {ι : Type u_2} [Countable ι] {μ : ι → Measure α} : (sum μ).MutuallySingular ν ↔ ∀ (i : ι), (μ i).MutuallySingular ν

@[simp]

theorem MeasureTheory.Measure.MutuallySingular.sum_right {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {ι : Type u_2} [Countable ι] {ν : ι → Measure α} : μ.MutuallySingular (sum ν) ↔ ∀ (i : ι), μ.MutuallySingular (ν i)

@[simp]

theorem MeasureTheory.Measure.MutuallySingular.add_left_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ₁ μ₂ ν : Measure α} : (μ₁ + μ₂).MutuallySingular ν ↔ μ₁.MutuallySingular ν ∧ μ₂.MutuallySingular ν

@[simp]

theorem MeasureTheory.Measure.MutuallySingular.add_right_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ ν₁ ν₂ : Measure α} : μ.MutuallySingular (ν₁ + ν₂) ↔ μ.MutuallySingular ν₁ ∧ μ.MutuallySingular ν₂

theorem MeasureTheory.Measure.MutuallySingular.add_left {α : Type u_1} {m0 : MeasurableSpace α} {μ ν₁ ν₂ : Measure α} (h₁ : ν₁.MutuallySingular μ) (h₂ : ν₂.MutuallySingular μ) : (ν₁ + ν₂).MutuallySingular μ

theorem MeasureTheory.Measure.MutuallySingular.add_right {α : Type u_1} {m0 : MeasurableSpace α} {μ ν₁ ν₂ : Measure α} (h₁ : μ.MutuallySingular ν₁) (h₂ : μ.MutuallySingular ν₂) : μ.MutuallySingular (ν₁ + ν₂)

theorem MeasureTheory.Measure.MutuallySingular.smul {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} (r : ENNReal) (h : ν.MutuallySingular μ) : (r • ν).MutuallySingular μ

theorem MeasureTheory.Measure.MutuallySingular.smul_nnreal {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} (r : NNReal) (h : ν.MutuallySingular μ) : (r • ν).MutuallySingular μ

theorem MeasureTheory.Measure.MutuallySingular.restrict {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} (h : μ.MutuallySingular ν) (s : Set α) : (μ.restrict s).MutuallySingular ν

theorem MeasureTheory.Measure.eq_zero_of_absolutelyContinuous_of_mutuallySingular {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} (h_ac : μ.AbsolutelyContinuous ν) (h_ms : μ.MutuallySingular ν) : μ = 0

theorem MeasureTheory.Measure.absolutelyContinuous_of_add_of_mutuallySingular {α : Type u_1} {m0 : MeasurableSpace α} {μ ν₁ ν₂ : Measure α} (h : μ.AbsolutelyContinuous (ν₁ + ν₂)) (h_ms : μ.MutuallySingular ν₂) : μ.AbsolutelyContinuous ν₁

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 ν)

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 * ↑ε

theorem MeasureTheory.Measure.mutuallySingular_of_disjoint {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} (h : Disjoint μ ν) : μ.MutuallySingular ν

theorem MeasureTheory.Measure.MutuallySingular.disjoint {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} (h : μ.MutuallySingular ν) : Disjoint μ ν

theorem MeasureTheory.Measure.MutuallySingular.disjoint_ae {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} (h : μ.MutuallySingular ν) : Disjoint (ae μ) (ae ν)

theorem MeasureTheory.Measure.disjoint_of_disjoint_ae {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} (h : Disjoint (ae μ) (ae ν)) : Disjoint μ ν

theorem MeasureTheory.Measure.mutuallySingular_tfae {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} : [μ.MutuallySingular ν, Disjoint μ ν, Disjoint (ae μ) (ae ν)].TFAE

theorem MeasureTheory.Measure.mutuallySingular_iff_disjoint {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} : μ.MutuallySingular ν ↔ Disjoint μ ν

theorem MeasureTheory.Measure.mutuallySingular_iff_disjoint_ae {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} : μ.MutuallySingular ν ↔ Disjoint (ae μ) (ae ν)