Documentation

Mathlib.MeasureTheory.Measure.MutuallySingular

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

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

Equations
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
    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) :
      μ.MutuallySingular ν
      def MeasureTheory.Measure.MutuallySingular.nullSet {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (h : μ.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 : μ.MutuallySingular ν) :
        MeasurableSet h.nullSet
        @[simp]
        theorem MeasureTheory.Measure.MutuallySingular.measure_nullSet {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (h : μ.MutuallySingular ν) :
        μ h.nullSet = 0
        @[simp]
        theorem MeasureTheory.Measure.MutuallySingular.measure_compl_nullSet {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (h : μ.MutuallySingular ν) :
        ν h.nullSet = 0
        @[simp]
        theorem MeasureTheory.Measure.MutuallySingular.restrict_nullSet {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (h : μ.MutuallySingular ν) :
        μ.restrict h.nullSet = 0
        @[simp]
        theorem MeasureTheory.Measure.MutuallySingular.restrict_compl_nullSet {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (h : μ.MutuallySingular ν) :
        ν.restrict h.nullSet = 0
        @[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 α} {ν : MeasureTheory.Measure α} (h : ν.MutuallySingular μ) :
        μ.MutuallySingular ν
        theorem MeasureTheory.Measure.MutuallySingular.comm {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} :
        μ.MutuallySingular ν ν.MutuallySingular μ
        theorem MeasureTheory.Measure.MutuallySingular.mono_ac {α : Type u_1} {m0 : MeasurableSpace α} {μ₁ : MeasureTheory.Measure α} {μ₂ : MeasureTheory.Measure α} {ν₁ : MeasureTheory.Measure α} {ν₂ : MeasureTheory.Measure α} (h : μ₁.MutuallySingular ν₁) (hμ : μ₂.AbsolutelyContinuous μ₁) (hν : ν₂.AbsolutelyContinuous ν₁) :
        μ₂.MutuallySingular ν₂
        theorem MeasureTheory.Measure.MutuallySingular.mono {α : Type u_1} {m0 : MeasurableSpace α} {μ₁ : MeasureTheory.Measure α} {μ₂ : MeasureTheory.Measure α} {ν₁ : MeasureTheory.Measure α} {ν₂ : MeasureTheory.Measure α} (h : μ₁.MutuallySingular ν₁) (hμ : μ₂ μ₁) (hν : ν₂ ν₁) :
        μ₂.MutuallySingular ν₂
        @[simp]
        theorem MeasureTheory.Measure.MutuallySingular.self_iff {α : Type u_1} {m0 : MeasurableSpace α} (μ : 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.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 α} {μ₂ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} :
        (μ₁ + μ₂).MutuallySingular ν μ₁.MutuallySingular ν μ₂.MutuallySingular ν
        @[simp]
        theorem MeasureTheory.Measure.MutuallySingular.add_right_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν₁ : MeasureTheory.Measure α} {ν₂ : MeasureTheory.Measure α} :
        μ.MutuallySingular (ν₁ + ν₂) μ.MutuallySingular ν₁ μ.MutuallySingular ν₂
        theorem MeasureTheory.Measure.MutuallySingular.add_left {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν₁ : MeasureTheory.Measure α} {ν₂ : MeasureTheory.Measure α} (h₁ : ν₁.MutuallySingular μ) (h₂ : ν₂.MutuallySingular μ) :
        (ν₁ + ν₂).MutuallySingular μ
        theorem MeasureTheory.Measure.MutuallySingular.add_right {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν₁ : MeasureTheory.Measure α} {ν₂ : MeasureTheory.Measure α} (h₁ : μ.MutuallySingular ν₁) (h₂ : μ.MutuallySingular ν₂) :
        μ.MutuallySingular (ν₁ + ν₂)
        theorem MeasureTheory.Measure.MutuallySingular.smul {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (r : ENNReal) (h : ν.MutuallySingular μ) :
        (r ν).MutuallySingular μ
        theorem MeasureTheory.Measure.MutuallySingular.smul_nnreal {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (r : NNReal) (h : ν.MutuallySingular μ) :
        (r ν).MutuallySingular μ
        theorem MeasureTheory.Measure.MutuallySingular.restrict {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : 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 α} {ν : MeasureTheory.Measure α} (h_ac : μ.AbsolutelyContinuous ν) (h_ms : μ.MutuallySingular ν) :
        μ = 0
        theorem MeasurableEmbedding.mutuallySingular_map {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {β : Type u_2} :
        ∀ {x : MeasurableSpace β} {f : αβ}, MeasurableEmbedding fμ.MutuallySingular ν(MeasureTheory.Measure.map f μ).MutuallySingular (MeasureTheory.Measure.map f ν)