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 α → MeasureTheory.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
- MeasureTheory.Measure.MutuallySingular μ ν = ∃ (s : Set α), MeasurableSet s ∧ ↑↑μ s = 0 ∧ ↑↑ν 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
- One or more equations did not get rendered due to their size.
Instances For
theorem
MeasureTheory.Measure.MutuallySingular.mk
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
(hs : ↑↑μ s = 0)
(ht : ↑↑ν t = 0)
(hst : Set.univ ⊆ s ∪ t)
:
def
MeasureTheory.Measure.MutuallySingular.nullSet
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
(h : MeasureTheory.Measure.MutuallySingular μ ν)
:
Set α
A set such that μ h.nullSet = 0 and ν h.nullSetᶜ = 0.
Equations
Instances For
theorem
MeasureTheory.Measure.MutuallySingular.measurableSet_nullSet
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
(h : MeasureTheory.Measure.MutuallySingular μ ν)
:
@[simp]
theorem
MeasureTheory.Measure.MutuallySingular.measure_nullSet
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
(h : MeasureTheory.Measure.MutuallySingular μ ν)
:
@[simp]
theorem
MeasureTheory.Measure.MutuallySingular.measure_compl_nullSet
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
(h : MeasureTheory.Measure.MutuallySingular μ ν)
:
@[simp]
theorem
MeasureTheory.Measure.MutuallySingular.restrict_nullSet
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
(h : MeasureTheory.Measure.MutuallySingular μ ν)
:
μ.restrict (MeasureTheory.Measure.MutuallySingular.nullSet h) = 0
@[simp]
theorem
MeasureTheory.Measure.MutuallySingular.restrict_compl_nullSet
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
(h : MeasureTheory.Measure.MutuallySingular μ ν)
:
ν.restrict (MeasureTheory.Measure.MutuallySingular.nullSet h)ᶜ = 0
@[simp]
theorem
MeasureTheory.Measure.MutuallySingular.zero_right
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
:
theorem
MeasureTheory.Measure.MutuallySingular.symm
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
(h : MeasureTheory.Measure.MutuallySingular ν μ)
:
theorem
MeasureTheory.Measure.MutuallySingular.comm
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
:
@[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 α}
{μ₂ : MeasureTheory.Measure α}
{ν₁ : MeasureTheory.Measure α}
{ν₂ : MeasureTheory.Measure α}
(h : MeasureTheory.Measure.MutuallySingular μ₁ ν₁)
(hμ : MeasureTheory.Measure.AbsolutelyContinuous μ₂ μ₁)
(hν : MeasureTheory.Measure.AbsolutelyContinuous ν₂ ν₁)
:
theorem
MeasureTheory.Measure.MutuallySingular.mono
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ₁ : MeasureTheory.Measure α}
{μ₂ : MeasureTheory.Measure α}
{ν₁ : MeasureTheory.Measure α}
{ν₂ : MeasureTheory.Measure α}
(h : MeasureTheory.Measure.MutuallySingular μ₁ ν₁)
(hμ : μ₂ ≤ μ₁)
(hν : ν₂ ≤ ν₁)
:
@[simp]
theorem
MeasureTheory.Measure.MutuallySingular.self_iff
{α : Type u_1}
{m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
:
MeasureTheory.Measure.MutuallySingular μ μ ↔ μ = 0
@[simp]
theorem
MeasureTheory.Measure.MutuallySingular.sum_left
{α : Type u_1}
{m0 : MeasurableSpace α}
{ν : MeasureTheory.Measure α}
{ι : Type u_2}
[Countable ι]
{μ : ι → MeasureTheory.Measure α}
:
MeasureTheory.Measure.MutuallySingular (MeasureTheory.Measure.sum μ) ν ↔ ∀ (i : ι), MeasureTheory.Measure.MutuallySingular (μ i) ν
@[simp]
theorem
MeasureTheory.Measure.MutuallySingular.sum_right
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ι : Type u_2}
[Countable ι]
{ν : ι → MeasureTheory.Measure α}
:
MeasureTheory.Measure.MutuallySingular μ (MeasureTheory.Measure.sum ν) ↔ ∀ (i : ι), MeasureTheory.Measure.MutuallySingular μ (ν i)
@[simp]
theorem
MeasureTheory.Measure.MutuallySingular.add_left_iff
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ₁ : MeasureTheory.Measure α}
{μ₂ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
:
@[simp]
theorem
MeasureTheory.Measure.MutuallySingular.add_right_iff
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν₁ : MeasureTheory.Measure α}
{ν₂ : MeasureTheory.Measure α}
:
theorem
MeasureTheory.Measure.MutuallySingular.add_left
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν₁ : MeasureTheory.Measure α}
{ν₂ : MeasureTheory.Measure α}
(h₁ : MeasureTheory.Measure.MutuallySingular ν₁ μ)
(h₂ : MeasureTheory.Measure.MutuallySingular ν₂ μ)
:
MeasureTheory.Measure.MutuallySingular (ν₁ + ν₂) μ
theorem
MeasureTheory.Measure.MutuallySingular.add_right
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν₁ : MeasureTheory.Measure α}
{ν₂ : MeasureTheory.Measure α}
(h₁ : MeasureTheory.Measure.MutuallySingular μ ν₁)
(h₂ : MeasureTheory.Measure.MutuallySingular μ ν₂)
:
MeasureTheory.Measure.MutuallySingular μ (ν₁ + ν₂)
theorem
MeasureTheory.Measure.MutuallySingular.smul
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
(r : ENNReal)
(h : MeasureTheory.Measure.MutuallySingular ν μ)
:
theorem
MeasureTheory.Measure.MutuallySingular.smul_nnreal
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
(r : NNReal)
(h : MeasureTheory.Measure.MutuallySingular ν μ)
:
theorem
MeasureTheory.Measure.MutuallySingular.restrict
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
(h : MeasureTheory.Measure.MutuallySingular μ ν)
(s : Set α)
:
MeasureTheory.Measure.MutuallySingular (μ.restrict s) ν
theorem
MeasureTheory.Measure.eq_zero_of_absolutelyContinuous_of_mutuallySingular
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
(h_ac : MeasureTheory.Measure.AbsolutelyContinuous μ ν)
(h_ms : MeasureTheory.Measure.MutuallySingular μ ν)
:
μ = 0