Randomness and Solovay degrees

Miyabe, Nies, Stephan

Page 3 says:

We sometimes identify a real α with its binary expansion X ∈ 2^ω and the corresponding set X = {n ∈ ℕ : X (n) = 1 }

Here we prove the well known fact that this representation is not unique.

We also show that consequently, if we use Mathlib's current definition of the pullback measure as of June 23, 2024 as a basis for a measure on Cantor space, the Cantor space gets measure 0.

However, if we use Etienne Marion's KolmogorovExtension4 library things work out well.

theorem tsum_geometric_two_succ : ∑' (n : ℕ), 1 / 2 ^ n.succ = 1

theorem geom_summable : Summable fun (n : ℕ) => 1 / 2 ^ n.succ

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

Equations

• CantorLebesgueMeasure₀ = MeasureTheory.Measure.comap real_of_cantor MeasureTheory.volume

def halfminus (n : ℕ) : Bool

Equations

• halfminus n = if n = 0 then false else true

def halfplus (n : ℕ) : Bool

Equations

• halfplus n = if n = 0 then true else false

theorem halfplus_ne_halfminus : halfplus ≠ halfminus

theorem real_of_cantor_noninjective : real_of_cantor halfminus = real_of_cantor halfplus

noncomputable def fairCoin'' : PMF Bool

Equations

• fairCoin'' = PMF.bernoulli (1 / 2) fairCoin''._proof_2

noncomputable def fairCoin : PMF Bool

Equations

• fairCoin = ⟨fun (b : Bool) => 1 / 2, fairCoin._proof_1⟩

noncomputable def β : MeasureTheory.ProbabilityMeasure Bool

Equations

• β = ⟨fairCoin.toMeasure, ⋯⟩

noncomputable def β' : MeasureTheory.ProbabilityMeasure Bool

Equations

• β' = ⟨fairCoin''.toMeasure, ⋯⟩

noncomputable def β'measure (p : NNReal) (hp : p ≤ 1) : MeasureTheory.ProbabilityMeasure Bool

Equations

• β'measure p hp = ⟨(PMF.bernoulli p hp).toMeasure, ⋯⟩

instance instIsProbabilityMeasureBoolValMeasureβ (n : ℕ) : MeasureTheory.IsProbabilityMeasure ((fun (x : ℕ) => ↑β) n)

theorem fairValue (b : Bool) : fairCoin b = 1 / 2

theorem fairValue'' (b : Bool) : fairCoin'' b = 1 / 2

theorem bernoulliValueTrue'' (p : NNReal) (hp : p ≤ 1) : (PMF.bernoulli p hp) true = ↑p

theorem bernoulliValueFalse'' (p : NNReal) (hp : p ≤ 1) : (PMF.bernoulli p hp) false = 1 - ↑p

theorem bernoulliSingletonTrue'' (p : NNReal) (hp : p ≤ 1) : (β'measure p hp) {true} = p

theorem bernoulliSingletonFalse'' (p : NNReal) (hp : p ≤ 1) : (β'measure p hp) {false} = 1 - p

theorem fairSingleton'' (b : Bool) : β' {b} = 1 / 2

theorem fairSingleton (b : Bool) : β {b} = 1 / 2

noncomputable instance instPseudoEMetricSpaceBool_marginis : PseudoEMetricSpace Bool

Equations

• instPseudoEMetricSpaceBool_marginis = MetricSpace.toEMetricSpace.toPseudoEMetricSpace

noncomputable def μ_bernoulli (p : NNReal) (hp : p ≤ 1) : MeasureTheory.Measure ((i : ℕ) → (fun (x : ℕ) => Bool) i)

The Bernoulli measure with parameter p.

Equations

• μ_bernoulli p hp = MeasureTheory.Measure.infinitePi fun (x : ℕ) => ↑(β'measure p hp)

instance instIsProbabilityMeasureForallBoolμ_bernoulli (p : NNReal) (hp : p ≤ 1) : MeasureTheory.IsProbabilityMeasure (μ_bernoulli p hp)

theorem bernoulliUniv'' (p : NNReal) (hp : p ≤ 1) : (μ_bernoulli p hp) Set.univ = 1