A small positive measurable set from non-atomicity

This file proves that on a standard Borel probability space (α, μ) whose measure μ has no atoms, for every threshold δ > 0 there is a measurable set A with 0 < μ A < δ (Oseledets.Krieger.exists_small_pos_measurableSet).

This statement is genuinely absent from Mathlib: the docstring of Mathlib/MeasureTheory/Measure/Typeclasses/NoAtoms.lean records, as an open TODO, the question of whether NoAtoms should be strengthened to the divisibility property ∀ s, 0 < μ s → ∃ t ⊆ s, 0 < μ t ∧ μ t < μ s, of which the result here is the global instance (s = univ). No constructive small-positive-set lemma exists in the library, so we build one from scratch.

Construction

We use the measurable embedding f := MeasureTheory.embeddingReal α : α → ℝ of the standard Borel space α into the reals (MeasureTheory.measurableEmbedding_embeddingReal). For a level n : ℕ and an integer k : ℤ, the dyadic cell

dyadicCell f n k := f ⁻¹' Set.Ico ((k : ℝ) / 2 ^ n) ((k + 1) / 2 ^ n)

is the f-preimage of a half-open dyadic interval. The cell at level n through a point x is dyadicCell f n ⌊f x * 2 ^ n⌋; equivalently it is {y | ⌊f y * 2 ^ n⌋ = ⌊f x * 2 ^ n⌋}. These cells through a fixed x are measurable, contain x, are nested decreasingly in n, and shrink to {x} (because f is injective and the intervals have radius 2 ^ (-n) → 0); hence their measure tends to 0 by continuity from above. The set

Z := {x | ∃ n, μ (dyadicCell f n ⌊f x * 2 ^ n⌋) = 0}

is contained in a countable union of null dyadic cells, so μ Z = 0 < μ univ; picking x ∉ Z makes every cell through x have positive measure, while the measure still tends to 0, so some cell has measure in (0, δ).

Main statement

• Oseledets.Krieger.exists_small_pos_measurableSet : on a standard Borel probability space with a non-atomic measure, every positive threshold bounds a positive-measure measurable set from below.

This is a building block for the Rokhlin tower / Krieger generator development (issue #15).

def Oseledets.Krieger.dyadicCell {α : Type u_1} (f : α → ℝ) (n : ℕ) (k : ℤ) : Set α

The dyadic cell at level n and index k: the f-preimage of the half-open dyadic interval [k / 2 ^ n, (k + 1) / 2 ^ n).

Equations

• Oseledets.Krieger.dyadicCell f n k = f ⁻¹' Set.Ico (↑k / 2 ^ n) ((↑k + 1) / 2 ^ n)

def Oseledets.Krieger.cell {α : Type u_1} (f : α → ℝ) (n : ℕ) (x : α) : Set α

The dyadic cell at level n through the point x: the cell whose index is the floor of f x * 2 ^ n. Equivalently {y | ⌊f y * 2 ^ n⌋ = ⌊f x * 2 ^ n⌋} (see mem_cell).

Equations

• Oseledets.Krieger.cell f n x = Oseledets.Krieger.dyadicCell f n ⌊f x * 2 ^ n⌋

theorem Oseledets.Krieger.mem_dyadicCell {α : Type u_1} {f : α → ℝ} {n : ℕ} {k : ℤ} {y : α} : y ∈ dyadicCell f n k ↔ ⌊f y * 2 ^ n⌋ = k

A point y lies in the dyadic cell dyadicCell f n k iff ⌊f y * 2 ^ n⌋ = k.

theorem Oseledets.Krieger.measurableSet_dyadicCell {α : Type u_1} [MeasurableSpace α] {f : α → ℝ} (hf : Measurable f) (n : ℕ) (k : ℤ) : MeasurableSet (dyadicCell f n k)

Every dyadic cell is the f-preimage of a measurable set, hence measurable whenever f is.

theorem Oseledets.Krieger.mem_cell {α : Type u_1} {f : α → ℝ} {n : ℕ} {x y : α} : y ∈ cell f n x ↔ ⌊f y * 2 ^ n⌋ = ⌊f x * 2 ^ n⌋

Membership in the cell through x is equality of dyadic floors.

theorem Oseledets.Krieger.self_mem_cell {α : Type u_1} {f : α → ℝ} (n : ℕ) (x : α) : x ∈ cell f n x

x belongs to its own cell.

theorem Oseledets.Krieger.measurableSet_cell {α : Type u_1} [MeasurableSpace α] {f : α → ℝ} (hf : Measurable f) (n : ℕ) (x : α) : MeasurableSet (cell f n x)

The cell through x is measurable when f is.

theorem Oseledets.Krieger.cell_succ_subset {α : Type u_1} {f : α → ℝ} (n : ℕ) (x : α) : cell f (n + 1) x ⊆ cell f n x

Dyadic nesting. The level-(n+1) cell through x is contained in the level-n cell. The key arithmetic fact is ⌊t * 2 ^ n⌋ = ⌊t * 2 ^ (n+1)⌋ / 2 (Int.floor_div_natCast applied to t * 2 ^ (n+1) = (t * 2 ^ n) * 2), so equality of the finer floors forces equality of the coarser ones.

theorem Oseledets.Krieger.antitone_cell {α : Type u_1} {f : α → ℝ} (x : α) : Antitone fun (n : ℕ) => cell f n x

The cells through x form an antitone sequence in the level n.

theorem Oseledets.Krieger.iInter_cell_subset {α : Type u_1} {f : α → ℝ} (hf : Function.Injective f) (x : α) : ⋂ (n : ℕ), cell f n x ⊆ {x}

Cells shrink to the point. Any y in every cell through x satisfies f y = f x: for each n, both f y * 2 ^ n and f x * 2 ^ n lie in [k, k + 1) for the common floor k, so they are within distance 1, i.e. |f y - f x| < 2 ^ (-n), which forces f y = f x as n → ∞.

theorem Oseledets.Krieger.tendsto_measure_cell {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.NoAtoms μ] (hf : MeasurableEmbedding (MeasureTheory.embeddingReal α)) (x : α) : Filter.Tendsto (fun (n : ℕ) => μ (cell (MeasureTheory.embeddingReal α) n x)) Filter.atTop (nhds 0)

Continuity from above for cells. The measure of the cell through x tends to 0: the cells are antitone and shrink to (a subset of) {x}, a null set under NoAtoms, so by continuity from above (tendsto_measure_iInter_atTop) the measures converge to μ (⋂ n, cell f n x) = 0.

theorem Oseledets.Krieger.exists_small_pos_measurableSet {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.NoAtoms μ] {δ : ENNReal} (hδ : 0 < δ) : ∃ (A : Set α), MeasurableSet A ∧ 0 < μ A ∧ μ A < δ

Small positive measurable set.

On a standard Borel probability space whose measure μ has no atoms, for every threshold δ > 0 there is a measurable set A with 0 < μ A and μ A < δ.

This fills a gap in Mathlib: the NoAtoms file's TODO notes that the divisibility property ∀ s, 0 < μ s → ∃ t ⊆ s, 0 < μ t < μ s (of which this is the s = univ instance) is not part of the library. The construction is via the measurable embedding MeasureTheory.embeddingReal into the reals and the dyadic cells dyadicCell/cell built from it. It is a building block for the Rokhlin tower / Krieger generator development (issue #15).