A computational aspect of the Lebesgue differentiation theorem

by NOOPUR PATHAK

She writes Another characterization of random points in ℝ^d is given by Solovay's Lemma. [...] The proof given by Simpson is given for sets in the Cantor space, but the proof applies here as well.

Here we expound this by constructing the Cantor-Lebesgue measure on 2^ω using the Lebesgue measure on [0,1].

[ Related Marginis entries: Miyabe, Nies, Stephan: Randomness and Solovay degrees at https://github.com/bjoernkjoshanssen/jla/blob/main/2018-miyabe-nies-stephan.lean (proving that the usual map from 2^omega to [0,1] is not injective) and Pauly and Fouche at https://github.com/bjoernkjoshanssen/jla/blob/main/2017-pauly-fouche.lean (constructing the Cantor-Hausdorff measure on 2^ω, which does coincide with the Cantor-Lebesgue measure) ]

noncomputable def real_of_cantor : (ℕ → Bool) → ℝ

Equations

• real_of_cantor x = ∑' (n : ℕ), if x n = true then 1 / 2 ^ n.succ else 0

noncomputable def CantorLebesgueMeasureSubtype : MeasureTheory.Measure { x : ℕ → Bool // ¬∃ (k : ℕ), x k = false ∧ ∀ (l : ℕ), k < l → x l = true }

Equations

• CantorLebesgueMeasureSubtype = MeasureTheory.Measure.comap (fun (x : { x : ℕ → Bool // ¬∃ (k : ℕ), x k = false ∧ ∀ (l : ℕ), k < l → x l = true }) => real_of_cantor ↑x) MeasureTheory.volume

noncomputable def CantorLebesgueMeasure : MeasureTheory.Measure (ℕ → Bool)

Equations

• CantorLebesgueMeasure = MeasureTheory.Measure.map (fun (x : { x : ℕ → Bool // ¬∃ (k : ℕ), x k = false ∧ ∀ (l : ℕ), k < l → x l = true }) => ↑x) CantorLebesgueMeasureSubtype