Documentation

Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass

Measures having value zero on singletons #

TODO #

Add a NoAtoms class defined as ∀ s, MeasurableSet s → 0 < μ s → ∃ t ⊆ s, MeasurableSet t ∧ 0 < μ t ∧ μ t < μ s. This implies NullSingletonClass but the converse is not true.

source
class MeasureTheory.NullSingletonClass {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) :
Prop

Measure μ has value zero on singletons.

  • measure_singleton (x : α) : μ {x} = 0
Instances
    source
    @[deprecated MeasureTheory.NullSingletonClass (since := "2026-06-09")]
    def MeasureTheory.NoAtoms {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) :
    Prop

    Alias of MeasureTheory.NullSingletonClass.

    Measure μ has value zero on singletons.

    Equations
    Instances For
      source
      theorem Set.Subsingleton.measure_zero {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α} (hs : s.Subsingleton) (μ : MeasureTheory.Measure α) [MeasureTheory.NullSingletonClass μ] :
      μ s = 0
      source
      theorem MeasureTheory.Measure.restrict_singleton' {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] {a : α} :
      μ.restrict {a} = 0
      source
      instance MeasureTheory.Measure.restrict.instNullSingletonClass {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] (s : Set α) :
      NullSingletonClass (μ.restrict s)
      source
      theorem Set.Countable.measure_zero {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α} (h : s.Countable) (μ : MeasureTheory.Measure α) [MeasureTheory.NullSingletonClass μ] :
      μ s = 0
      source
      theorem Set.Countable.ae_notMem {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α} (h : s.Countable) (μ : MeasureTheory.Measure α) [MeasureTheory.NullSingletonClass μ] :
      ∀ᵐ (x : α) ∂μ, x ∉ s
      source
      theorem MeasureTheory.Measure.ae_ne {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) [NullSingletonClass μ] (a : α) :
      ∀ᵐ (x : α) ∂μ, x ≠ a
      source
      theorem Set.Countable.measure_restrict_compl {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α} (h : s.Countable) (μ : MeasureTheory.Measure α) [MeasureTheory.NullSingletonClass μ] :
      μ.restrict sᶜ = μ
      source
      @[simp]
      theorem MeasureTheory.restrict_compl_singleton {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] (a : α) :
      μ.restrict {a}ᶜ = μ
      source
      theorem Set.Finite.measure_zero {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α} (h : s.Finite) (μ : MeasureTheory.Measure α) [MeasureTheory.NullSingletonClass μ] :
      μ s = 0
      source
      theorem Finset.measure_zero {α : Type u_1} {m0 : MeasurableSpace α} (s : Finset α) (μ : MeasureTheory.Measure α) [MeasureTheory.NullSingletonClass μ] :
      μ ↑s = 0
      source
      theorem MeasureTheory.insert_ae_eq_self {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] (a : α) (s : Set α) :
      insert a s =ᵐ[μ] s
      source
      theorem MeasureTheory.exists_accPt_of_nullSingletonClass {X : Type u_2} [TopologicalSpace X] [MeasurableSpace X] {μ : Measure X} [NullSingletonClass μ] {E : Set X} [TopologicalSpace.SeparableSpace ↑E] (hE : 0 < μ E) :
      ∃ (x : X), AccPt x (Filter.principal E)
      source
      @[deprecated MeasureTheory.exists_accPt_of_nullSingletonClass (since := "2026-06-09")]
      theorem MeasureTheory.exists_accPt_of_noAtoms {X : Type u_2} [TopologicalSpace X] [MeasurableSpace X] {μ : Measure X} [NullSingletonClass μ] {E : Set X} [TopologicalSpace.SeparableSpace ↑E] (hE : 0 < μ E) :
      ∃ (x : X), AccPt x (Filter.principal E)

      Alias of MeasureTheory.exists_accPt_of_nullSingletonClass.

      source
      theorem MeasureTheory.Iio_ae_eq_Iic {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] [PartialOrder α] {a : α} :
      Set.Iio a =ᵐ[μ] Set.Iic a
      source
      theorem MeasureTheory.Ioi_ae_eq_Ici {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] [PartialOrder α] {a : α} :
      Set.Ioi a =ᵐ[μ] Set.Ici a
      source
      theorem MeasureTheory.Ioo_ae_eq_Ioc {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] [PartialOrder α] {a b : α} :
      Set.Ioo a b =ᵐ[μ] Set.Ioc a b
      source
      theorem MeasureTheory.Ioc_ae_eq_Icc {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] [PartialOrder α] {a b : α} :
      Set.Ioc a b =ᵐ[μ] Set.Icc a b
      source
      theorem MeasureTheory.Ioo_ae_eq_Ico {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] [PartialOrder α] {a b : α} :
      Set.Ioo a b =ᵐ[μ] Set.Ico a b
      source
      theorem MeasureTheory.Ioo_ae_eq_Icc {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] [PartialOrder α] {a b : α} :
      Set.Ioo a b =ᵐ[μ] Set.Icc a b
      source
      theorem MeasureTheory.Ico_ae_eq_Icc {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] [PartialOrder α] {a b : α} :
      Set.Ico a b =ᵐ[μ] Set.Icc a b
      source
      theorem MeasureTheory.Ico_ae_eq_Ioc {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] [PartialOrder α] {a b : α} :
      Set.Ico a b =ᵐ[μ] Set.Ioc a b
      source
      theorem MeasureTheory.restrict_Iio_eq_restrict_Iic {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] [PartialOrder α] {a : α} :
      μ.restrict (Set.Iio a) = μ.restrict (Set.Iic a)
      source
      theorem MeasureTheory.restrict_Ioi_eq_restrict_Ici {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] [PartialOrder α] {a : α} :
      μ.restrict (Set.Ioi a) = μ.restrict (Set.Ici a)
      source
      theorem MeasureTheory.restrict_Ioo_eq_restrict_Ioc {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] [PartialOrder α] {a b : α} :
      μ.restrict (Set.Ioo a b) = μ.restrict (Set.Ioc a b)
      source
      theorem MeasureTheory.restrict_Ioc_eq_restrict_Icc {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] [PartialOrder α] {a b : α} :
      μ.restrict (Set.Ioc a b) = μ.restrict (Set.Icc a b)
      source
      theorem MeasureTheory.restrict_Ioo_eq_restrict_Ico {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] [PartialOrder α] {a b : α} :
      μ.restrict (Set.Ioo a b) = μ.restrict (Set.Ico a b)
      source
      theorem MeasureTheory.restrict_Ioo_eq_restrict_Icc {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] [PartialOrder α] {a b : α} :
      μ.restrict (Set.Ioo a b) = μ.restrict (Set.Icc a b)
      source
      theorem MeasureTheory.restrict_Ico_eq_restrict_Icc {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] [PartialOrder α] {a b : α} :
      μ.restrict (Set.Ico a b) = μ.restrict (Set.Icc a b)
      source
      theorem MeasureTheory.restrict_Ico_eq_restrict_Ioc {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] [PartialOrder α] {a b : α} :
      μ.restrict (Set.Ico a b) = μ.restrict (Set.Ioc a b)
      source
      theorem MeasureTheory.uIoc_ae_eq_interval {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NullSingletonClass μ] [LinearOrder α] {a b : α} :
      Set.uIoc a b =ᵐ[μ] Set.uIcc a b