Randomness and Solovay degrees

by

Miyabe, Nies, Stephan

JLA, 2018. 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

theorem because_real_of_cantor_not_injective : CantorLebesgueMeasure₀ Set.univ = 0

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_2⟩

noncomputable def β : MeasureTheory.ProbabilityMeasure Bool

Equations

• β = ⟨fairCoin.toMeasure, ⋯⟩

noncomputable def β' : MeasureTheory.ProbabilityMeasure Bool

Equations

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

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

Equations

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

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

Equations

• ⋯ = ⋯

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

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

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

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

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

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

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

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

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

The Bernoulli measure with parameter p.

Equations

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

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

Equations

• ⋯ = ⋯

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

noncomputable def μFair : MeasureTheory.Measure ((i : ℕ) → (fun (x : ℕ) => Bool) i)

Equations

• μFair = MeasureTheory.productMeasure fun (x : ℕ) => ↑β

noncomputable def μFair'' : MeasureTheory.Measure ((i : ℕ) → (fun (x : ℕ) => Bool) i)

Equations

• μFair'' = MeasureTheory.productMeasure fun (x : ℕ) => ↑β'

instance instIsProbabilityMeasureForallBoolμFair : MeasureTheory.IsProbabilityMeasure μFair

Equations

• instIsProbabilityMeasureForallBoolμFair = ⋯

instance instIsProbabilityMeasureForallBoolμFair'' : MeasureTheory.IsProbabilityMeasure μFair''

Equations

• instIsProbabilityMeasureForallBoolμFair'' = ⋯

theorem fairUniv : μFair Set.univ = 1

theorem fairUniv'' : μFair'' Set.univ = 1

theorem trueμ_bernoulli (p : ENNReal) (hp : p ≤ 1) (k : ℕ) : (μ_bernoulli p hp) {A : (i : ℕ) → (fun (x : ℕ) => Bool) i | A k = true} = p

theorem falseμ_bernoulli (p : ENNReal) (hp : p ≤ 1) (k : ℕ) : (μ_bernoulli p hp) {A : (i : ℕ) → (fun (x : ℕ) => Bool) i | A k = false} = 1 - p

theorem fairHalf (b : Bool) (k : ℕ) : μFair {A : (i : ℕ) → (fun (x : ℕ) => Bool) i | A k = b} = 1 / 2

theorem bernoulliBoxes'' {s : ℕ} (b : Fin s → Bool) (p : ENNReal) (hp : p ≤ 1) : ∏ x ∈ Finset.Iio s, ↑(β'measure p hp) (if h : x < s then {b ⟨x, h⟩} else {false, true}) = p ^ (Finset.filter (fun (t : Fin s) => b t = true) Finset.univ).card * (1 - p) ^ (Finset.filter (fun (t : Fin s) => b t = false) Finset.univ).card

Progress since this one is based on PMF.bernoulli

theorem bernoulliBoxes''' {s : ℕ} (b : Fin s → Bool) (p : ENNReal) (hp : p ≤ 1) : (μ_bernoulli p hp) {A : ℕ → Bool | ∀ (k : Fin s), A ↑k = b k} = p ^ (Finset.filter (fun (t : Fin s) => b t = true) Finset.univ).card * (1 - p) ^ (Finset.filter (fun (t : Fin s) => b t = false) Finset.univ).card

Bernoulli measure of boxes.

theorem noAtomsReal (p : ℝ) (ε : ℝ) (h₀ : 0 < p) (h₁ : p < 1) (h : 0 < ε) : ∃ (n : ℕ), p ^ n ≤ ε

theorem noAtomsNNReal (ε : NNReal) (p : ℝ) (h₀ : 0 < p) (h₁ : p < 1) (h : 0 < ε) : ∃ (n : ℕ), p ^ n ≤ ↑ε

theorem noAtomsENNReal {ε : ENNReal} (H : ε ≠ ⊤) {p : ℝ} (h₀ : 0 < p) (h₁ : p < 1) (h : 0 < ε) : ∃ (n : ℕ), p ^ n ≤ ε.toReal

theorem extracted_1 (B : ℕ → Bool) (p : NNReal) (hp : p ≤ 1) (ε : ENNReal) (n₀ : ℕ) (hn₀ : ↑p ^ n₀ ≤ ε.toReal) (n₁ : ℕ) (z : Bool) (m : ENNReal) (this : m ≤ ↑p ^ (Finset.filter (fun (t : Fin (2 * max n₀ n₁)) => B ↑t = z) Finset.univ).card * (1 - ↑p) ^ (Finset.filter (fun (t : Fin (2 * max n₀ n₁)) => B ↑t = !z) Finset.univ).card) (h : (Finset.filter (fun (t : Fin (2 * max n₀ n₁)) => B ↑t = z) Finset.univ).card ≥ max n₀ n₁) : m ≤ ε

theorem binomial_left {p : ENNReal} (hp : p ≤ 1) {u : ℕ} {a : ℕ} (b : ℕ) (h : a ≥ u) : p ^ a * (1 - p) ^ b ≤ p ^ u

theorem binom_distr_left {B : ℕ → Bool} {p : ENNReal} (hp : p ≤ 1) {n₀ : ℕ} (u : ℕ) (hu : n₀ ≤ u) (z : Bool) (h : (Finset.filter (fun (t : Fin (2 * u)) => B ↑t = z) Finset.univ).card ≥ u) : p ^ (Finset.filter (fun (t : Fin (2 * u)) => B ↑t = z) Finset.univ).card * (1 - p) ^ (Finset.filter (fun (t : Fin (2 * u)) => B ↑t = !z) Finset.univ).card ≤ p ^ n₀

theorem binom_distr_left_est (B : ℕ → Bool) (p : ENNReal) (hp : p ≤ 1) (ε : ENNReal) (n₀ : ℕ) (hn₀ : p ^ n₀ ≤ ε) (n₁ : ℕ) (z : Bool) (m : ENNReal) (hm : m ≤ p ^ (Finset.filter (fun (t : Fin (2 * max n₀ n₁)) => B ↑t = z) Finset.univ).card * (1 - p) ^ (Finset.filter (fun (t : Fin (2 * max n₀ n₁)) => B ↑t = !z) Finset.univ).card) (h : (Finset.filter (fun (t : Fin (2 * max n₀ n₁)) => B ↑t = z) Finset.univ).card ≥ max n₀ n₁) : m ≤ ε

theorem majority (B : ℕ → Bool) (m : ℕ) : (Finset.filter (fun (t : Fin (2 * m)) => B ↑t = true) Finset.univ).card ≥ m ∨ (Finset.filter (fun (t : Fin (2 * m)) => B ↑t = false) Finset.univ).card ≥ m

theorem bound_of_toReal {ε : ENNReal} {p : ENNReal} (htop : p ≠ ⊤) {n₀ : ℕ} (hn : p.toReal ^ n₀ ≤ ε.toReal) : p ^ n₀ ≤ ε

theorem bernoulliNoAtoms {p : ENNReal} (hp : p ≤ 1) (hn₀ : 0 < p) (hn₁ : p < 1) (B : ℕ → Bool) : (μ_bernoulli p hp) {B} = 0

The Bernoulli measure with parameter p has no atoms.

theorem fairBoxes {s : ℕ} (b : Fin s → Bool) : μFair {A : (i : ℕ) → (fun (x : ℕ) => Bool) i | ∀ (k : Fin s), A ↑k = b k} = (1 / 2) ^ s

This mostly characterizes the measure.

instance γ : Group Bool

Equations

• γ = Group.mk γ.proof_10

instance instTopologicalGroupForallNatBool_marginis : TopologicalGroup (ℕ → Bool)

Equations

• instTopologicalGroupForallNatBool_marginis = ⋯

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

Equations

• ν = MeasureTheory.Measure.haarMeasure { carrier := Set.univ, isCompact' := ν.proof_2, interior_nonempty' := ν.proof_3 }