Mutually singular measures #
Two measures μ, ν are said to be mutually singular (measure_theory.measure.mutually_singular,
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
measure_theory.measure.mutually_singular.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 measure_theory.measure.mutually_singular and prove basic
facts about it.
Tags #
measure, mutually singular
def
measure_theory.measure.mutually_singular
{α : Type u_1}
{m0 : measurable_space α}
(μ ν : measure_theory.measure α) :
Prop
Two measures μ, ν are said to be mutually singular if there exists a measurable set s
such that μ s = 0 and ν sᶜ = 0.
theorem
measure_theory.measure.mutually_singular.mk
{α : Type u_1}
{m0 : measurable_space α}
{μ ν : measure_theory.measure α}
{s t : set α}
(hs : ⇑μ s = 0)
(ht : ⇑ν t = 0)
(hst : set.univ ⊆ s ∪ t) :
μ ⊥ₘ ν
@[simp]
theorem
measure_theory.measure.mutually_singular.zero_right
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α} :
μ ⊥ₘ 0
theorem
measure_theory.measure.mutually_singular.symm
{α : Type u_1}
{m0 : measurable_space α}
{μ ν : measure_theory.measure α}
(h : ν ⊥ₘ μ) :
μ ⊥ₘ ν
theorem
measure_theory.measure.mutually_singular.comm
{α : Type u_1}
{m0 : measurable_space α}
{μ ν : measure_theory.measure α} :
@[simp]
theorem
measure_theory.measure.mutually_singular.zero_left
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α} :
0 ⊥ₘ μ
theorem
measure_theory.measure.mutually_singular.mono_ac
{α : Type u_1}
{m0 : measurable_space α}
{μ₁ μ₂ ν₁ ν₂ : measure_theory.measure α}
(h : μ₁ ⊥ₘ ν₁)
(hμ : μ₂ ≪ μ₁)
(hν : ν₂ ≪ ν₁) :
μ₂ ⊥ₘ ν₂
theorem
measure_theory.measure.mutually_singular.mono
{α : Type u_1}
{m0 : measurable_space α}
{μ₁ μ₂ ν₁ ν₂ : measure_theory.measure α}
(h : μ₁ ⊥ₘ ν₁)
(hμ : μ₂ ≤ μ₁)
(hν : ν₂ ≤ ν₁) :
μ₂ ⊥ₘ ν₂
@[simp]
theorem
measure_theory.measure.mutually_singular.sum_left
{α : Type u_1}
{m0 : measurable_space α}
{ν : measure_theory.measure α}
{ι : Type u_2}
[encodable ι]
{μ : ι → measure_theory.measure α} :
measure_theory.measure.sum μ ⊥ₘ ν ↔ ∀ (i : ι), μ i ⊥ₘ ν
@[simp]
theorem
measure_theory.measure.mutually_singular.sum_right
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{ι : Type u_2}
[encodable ι]
{ν : ι → measure_theory.measure α} :
μ ⊥ₘ measure_theory.measure.sum ν ↔ ∀ (i : ι), μ ⊥ₘ ν i
@[simp]
theorem
measure_theory.measure.mutually_singular.add_left_iff
{α : Type u_1}
{m0 : measurable_space α}
{μ₁ μ₂ ν : measure_theory.measure α} :
@[simp]
theorem
measure_theory.measure.mutually_singular.add_right_iff
{α : Type u_1}
{m0 : measurable_space α}
{μ ν₁ ν₂ : measure_theory.measure α} :
theorem
measure_theory.measure.mutually_singular.add_left
{α : Type u_1}
{m0 : measurable_space α}
{μ ν₁ ν₂ : measure_theory.measure α}
(h₁ : ν₁ ⊥ₘ μ)
(h₂ : ν₂ ⊥ₘ μ) :
theorem
measure_theory.measure.mutually_singular.add_right
{α : Type u_1}
{m0 : measurable_space α}
{μ ν₁ ν₂ : measure_theory.measure α}
(h₁ : μ ⊥ₘ ν₁)
(h₂ : μ ⊥ₘ ν₂) :
theorem
measure_theory.measure.mutually_singular.smul
{α : Type u_1}
{m0 : measurable_space α}
{μ ν : measure_theory.measure α}
(r : ℝ≥0∞)
(h : ν ⊥ₘ μ) :
theorem
measure_theory.measure.mutually_singular.smul_nnreal
{α : Type u_1}
{m0 : measurable_space α}
{μ ν : measure_theory.measure α}
(r : ℝ≥0)
(h : ν ⊥ₘ μ) :