Measures having no atoms

def MeasureTheory.IsAtom {α : Type u_1} {m0 : MeasurableSpace α} (s : Set α) (μ : Measure α) : Prop

An atom of a measure μ is a measurable set s of positive measure for which all measurable subsets either have measure 0 or μ s.

Equations

• MeasureTheory.IsAtom s μ = (MeasurableSet s ∧ 0 < μ s ∧ ∀ t ⊆ s, MeasurableSet t → μ t = 0 ∨ μ t = μ s)

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

Measure μ has no atoms if for any measurable set s with positive μ-measure, there exists a measurable t ⊆ s such that 0 < μ t < μ s. While this implies μ {x} = 0 under mild assumptions, the converse is not true.

• no_atoms (s : Set α) : ¬IsAtom s μ

theorem MeasureTheory.no_atoms_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} : NoAtoms' μ ↔ ∀ (s : Set α), MeasurableSet s → 0 < μ s → ∃ t ⊆ s, MeasurableSet t ∧ 0 < μ t ∧ μ t < μ s

theorem MeasureTheory.NoAtoms'.mk' {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} (h : ∀ (s : Set α), MeasurableSet s → 0 < μ s → ∃ t ⊆ s, 0 < μ t ∧ μ t < μ s) : NoAtoms' μ

theorem MeasureTheory.NoAtoms'.exists_measurable_subset_lt {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [na : NoAtoms' μ] {s : Set α} (meas_s : MeasurableSet s) (hs : 0 < μ s) : ∃ t ⊆ s, MeasurableSet t ∧ 0 < μ t ∧ μ t < μ s

theorem MeasureTheory.NoAtoms'.exists_measurable_subset_lt₀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [na : NoAtoms' μ] {s : Set α} (meas_s : NullMeasurableSet s μ) (hs : 0 < μ s) : ∃ t ⊆ s, MeasurableSet t ∧ 0 < μ t ∧ μ t < μ s

instance MeasureTheory.NoAtoms'.instNullSingletonClass {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [na : NoAtoms' μ] [MeasurableSingletonClass (NullMeasurableSpace α μ)] : NullSingletonClass μ

instance MeasureTheory.NoAtoms'.instNullSingletonClass' {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [na : NoAtoms' μ] [SigmaFinite μ] : NullSingletonClass μ

theorem MeasureTheory.NoAtoms'.restrict {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [na : NoAtoms' μ] (s : Set α) (hs : NullMeasurableSet s μ) : NoAtoms' (μ.restrict s)