Atomless measures

DefinitionAtomless measure#✓fully proved

A measure \(\mu\) on a measurable space is atomless when every measurable set \(s\) with \(\mu(s) > 0\) contains a measurable subset \(t \subseteq s\) with \(0 < \mu(t) < \mu(s)\).

def IsAtomless {α : Type*} [MeasurableSpace α] (μ : Measure α) : Prop :=
  ∀ s, MeasurableSet s → 0 < μ s → ∃ t, t ⊆ s ∧ MeasurableSet t ∧ 0 < μ t ∧ μ t < μ s

Used by 3

Used bySierpiński's theorem on atomless measures · Restriction of an atomless measure · Lyapunov convexity theorem

TheoremRestriction of an atomless measure#✓fully proved

The restriction of an atomless measure to a measurable set is atomless.

theorem isAtomless_restrict {α : Type*} [MeasurableSpace α] {μ : Measure α}
    {Z : Set α} (hZ : MeasurableSet Z) (hA : IsAtomless μ) :
    IsAtomless (μ.restrict Z)

Uses 1 · Used by 1

Statement usesAtomless measure

Used byLyapunov convexity theorem

TheoremSierpiński's theorem on atomless measures#✓fully proved

Let \(\mu\) be a finite atomless measure. For every measurable set \(s\) and every \(t \in [0, \infty]\) with \(t \le \mu(s)\), there is a measurable set \(u \subseteq s\) with \(\mu(u) = t\).

theorem isAtomless_exists_subset_measure_eq {α : Type*} [MeasurableSpace α]
    {μ : Measure α} [IsFiniteMeasure μ] (hA : IsAtomless μ)
    {s : Set α} (hs : MeasurableSet s) {t : ENNReal} (ht : t ≤ μ s) :
    ∃ u, u ⊆ s ∧ MeasurableSet u ∧ μ u = t

Uses 1 · Used by 1

Statement usesAtomless measure

Used byLyapunov convexity theorem

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.