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 α}
(μ ν : MeasureTheory.Measure α)
:
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.
Equations
- MeasureTheory.«term_⟂ₘ_» = Lean.ParserDescr.trailingNode `MeasureTheory.«term_⟂ₘ_» 60 60 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⟂ₘ ") (Lean.ParserDescr.cat `term 61))
Instances For
theorem
MeasureTheory.Measure.MutuallySingular.mk
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.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 α}
{μ ν : MeasureTheory.Measure α}
(h : μ.MutuallySingular ν)
:
Set α
A set such that μ h.nullSet = 0 and ν h.nullSetᶜ = 0.
Equations
- h.nullSet = Exists.choose h
Instances For
theorem
MeasureTheory.Measure.MutuallySingular.measurableSet_nullSet
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
(h : μ.MutuallySingular ν)
:
MeasurableSet h.nullSet
@[simp]
theorem
MeasureTheory.Measure.MutuallySingular.measure_nullSet
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
(h : μ.MutuallySingular ν)
:
μ h.nullSet = 0
@[simp]
theorem
MeasureTheory.Measure.MutuallySingular.measure_compl_nullSet
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
(h : μ.MutuallySingular ν)
:
@[simp]
theorem
MeasureTheory.Measure.MutuallySingular.restrict_nullSet
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
(h : μ.MutuallySingular ν)
:
μ.restrict h.nullSet = 0
@[simp]
theorem
MeasureTheory.Measure.MutuallySingular.restrict_compl_nullSet
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
(h : μ.MutuallySingular ν)
:
@[simp]
theorem
MeasureTheory.Measure.MutuallySingular.zero_right
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
:
μ.MutuallySingular 0
theorem
MeasureTheory.Measure.MutuallySingular.symm
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
(h : ν.MutuallySingular μ)
:
μ.MutuallySingular ν
theorem
MeasureTheory.Measure.MutuallySingular.comm
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
:
μ.MutuallySingular ν ↔ ν.MutuallySingular μ
@[simp]
theorem
MeasureTheory.Measure.MutuallySingular.zero_left
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
:
theorem
MeasureTheory.Measure.MutuallySingular.mono_ac
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ₁ μ₂ ν₁ ν₂ : MeasureTheory.Measure α}
(h : μ₁.MutuallySingular ν₁)
(hμ : μ₂.AbsolutelyContinuous μ₁)
(hν : ν₂.AbsolutelyContinuous ν₁)
:
μ₂.MutuallySingular ν₂
theorem
MeasureTheory.Measure.MutuallySingular.congr_ac
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ μ₂ ν ν₂ : MeasureTheory.Measure α}
(hμμ₂ : μ.AbsolutelyContinuous μ₂)
(hμ₂μ : μ₂.AbsolutelyContinuous μ)
(hνν₂ : ν.AbsolutelyContinuous ν₂)
(hν₂ν : ν₂.AbsolutelyContinuous ν)
:
μ.MutuallySingular ν ↔ μ₂.MutuallySingular ν₂
theorem
MeasureTheory.Measure.MutuallySingular.mono
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ₁ μ₂ ν₁ ν₂ : MeasureTheory.Measure α}
(h : μ₁.MutuallySingular ν₁)
(hμ : μ₂ ≤ μ₁)
(hν : ν₂ ≤ ν₁)
:
μ₂.MutuallySingular ν₂
@[simp]
theorem
MeasureTheory.Measure.MutuallySingular.self_iff
{α : Type u_1}
{m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
:
@[simp]
theorem
MeasureTheory.Measure.MutuallySingular.sum_left
{α : Type u_1}
{m0 : MeasurableSpace α}
{ν : MeasureTheory.Measure α}
{ι : Type u_2}
[Countable ι]
{μ : ι → MeasureTheory.Measure α}
:
(MeasureTheory.Measure.sum μ).MutuallySingular ν ↔ ∀ (i : ι), (μ i).MutuallySingular ν
@[simp]
theorem
MeasureTheory.Measure.MutuallySingular.sum_right
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ι : Type u_2}
[Countable ι]
{ν : ι → MeasureTheory.Measure α}
:
μ.MutuallySingular (MeasureTheory.Measure.sum ν) ↔ ∀ (i : ι), μ.MutuallySingular (ν i)
@[simp]
theorem
MeasureTheory.Measure.MutuallySingular.add_left_iff
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ₁ μ₂ ν : MeasureTheory.Measure α}
:
@[simp]
theorem
MeasureTheory.Measure.MutuallySingular.add_right_iff
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν₁ ν₂ : MeasureTheory.Measure α}
:
theorem
MeasureTheory.Measure.MutuallySingular.add_left
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν₁ ν₂ : MeasureTheory.Measure α}
(h₁ : ν₁.MutuallySingular μ)
(h₂ : ν₂.MutuallySingular μ)
:
(ν₁ + ν₂).MutuallySingular μ
theorem
MeasureTheory.Measure.MutuallySingular.add_right
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν₁ ν₂ : MeasureTheory.Measure α}
(h₁ : μ.MutuallySingular ν₁)
(h₂ : μ.MutuallySingular ν₂)
:
μ.MutuallySingular (ν₁ + ν₂)
theorem
MeasureTheory.Measure.MutuallySingular.smul
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
(r : ENNReal)
(h : ν.MutuallySingular μ)
:
(r • ν).MutuallySingular μ
theorem
MeasureTheory.Measure.MutuallySingular.smul_nnreal
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
(r : NNReal)
(h : ν.MutuallySingular μ)
:
(r • ν).MutuallySingular μ
theorem
MeasureTheory.Measure.MutuallySingular.restrict
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
(h : μ.MutuallySingular ν)
(s : Set α)
:
(μ.restrict s).MutuallySingular ν
theorem
MeasureTheory.Measure.eq_zero_of_absolutelyContinuous_of_mutuallySingular
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
(h_ac : μ.AbsolutelyContinuous ν)
(h_ms : μ.MutuallySingular ν)
:
μ = 0
theorem
MeasureTheory.Measure.absolutelyContinuous_of_add_of_mutuallySingular
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν₁ ν₂ : MeasureTheory.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 α}
{μ ν : MeasureTheory.Measure α}
(h : Disjoint μ ν)
{ε : NNReal}
(hε : 0 < ε)
:
theorem
MeasureTheory.Measure.mutuallySingular_of_disjoint
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
(h : Disjoint μ ν)
:
μ.MutuallySingular ν
theorem
MeasureTheory.Measure.MutuallySingular.disjoint
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
(h : μ.MutuallySingular ν)
:
Disjoint μ ν
theorem
MeasureTheory.Measure.MutuallySingular.disjoint_ae
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
(h : μ.MutuallySingular ν)
:
Disjoint (MeasureTheory.ae μ) (MeasureTheory.ae ν)
theorem
MeasureTheory.Measure.disjoint_of_disjoint_ae
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
(h : Disjoint (MeasureTheory.ae μ) (MeasureTheory.ae ν))
:
Disjoint μ ν
theorem
MeasureTheory.Measure.mutuallySingular_tfae
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
:
[μ.MutuallySingular ν, Disjoint μ ν, Disjoint (MeasureTheory.ae μ) (MeasureTheory.ae ν)].TFAE
theorem
MeasureTheory.Measure.mutuallySingular_iff_disjoint
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
:
theorem
MeasureTheory.Measure.mutuallySingular_iff_disjoint_ae
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
:
μ.MutuallySingular ν ↔ Disjoint (MeasureTheory.ae μ) (MeasureTheory.ae ν)