Probability space for infinite iid fair coin flips

Stream: maths

[John Tristan]

I am interested in learning about the different ways one can construct a probability space for infinite iid fair coin flips in lean4 and potentially using mathlib4.

I am currently doing it using a pre-existing formalization of the Caratheodory extension theorem and adapting from the algebra of sets described in Joe Hurd's dissertation on verification of randomized algorithms.

While it seems to me like a reasonable construction, I am wondering if perhaps this has already been done, or if there is a simpler way to do it. What made me wonder is a comment in mathlib4 just before an instance of a relevant measurable space.

Thank you.

[Thomas Zhu]

This has not been done, and the way you linked to would indeed be the easiest way to do it as of now (I think). I think the primary reason it is not done is that we want arbitrary (not just countable) products of probability spaces in full generality (see this).

[Thomas Zhu]

admittedly this is an overkill for countable iid Bernoulli which is easy from Caratheodory extension or Kolmogorov extension.

[Thomas Zhu]

The comment refers to the MeasurableSpace structure on Pi types Set a, i.e. a -> Prop (in your application Nat -> Bool), but no Measure is defined on this space yet

[Josha Dekker]

fwiw, iirc there is also a result that says something along the lines of that a space admits an infinite iid sequence of coin flips iff it admits a continuous random variable. Not sure what the result is called though

[Thomas Zhu]

related previous discussion

[Thomas Zhu]

Josha Dekker said:

fwiw, iirc there is also a result that says something along the lines of that a space admits an infinite iid sequence of coin flips iff it admits a continuous random variable. Not sure what the result is called though

I think that is just relating X ~ U([0,1]) to its binary expansion sequences (modulo cases of 0111... = 1000... which are only countably many hence null)

[Thomas Zhu]

Ah, maybe then a temporary workaround is you can define countable iid coin flips as pushforward of U([0,1]) through binary expansion. I'm not sure how easy it would be to prove properties of it

[Josha Dekker]

Thomas Zhu said:

Ah, maybe then a temporary workaround is you can define countable iid coin flips as pushforward of U([0,1]) through binary expansion. I'm not sure how easy it would be to prove properties of it

Yes, that is what I thought, so you don’t need to worry about products of probability spaces.

[Rémy Degenne]

I had a private discussion with John about this (I did not see this message when it was first posted). Let me repeat the main message of the discussion here: the repository he linked to contains a full proof of the Kolmogorov extension theorem, from which one can very easily get a measure for infinitely many coin flips. Here is some code to do that (with coin flips taking values in the reals):

import KolmogorovExtension4.independentFamily

open scoped NNReal

open MeasureTheory

variable {ι : Type*} [Nonempty ι]
  {α : ι → Type*} [∀ i, MeasurableSpace (α i)] [∀ i, TopologicalSpace (α i)]
  [∀ i, PolishSpace (α i)] [∀ i, Nonempty (α i)] [∀ i, BorelSpace (α i)]

noncomputable
def independentFamily' (P : ∀ i, Measure (α i)) [∀ i, IsProbabilityMeasure (P i)] :
    Measure (∀ i, α i) :=
  projectiveLimit (Measure.subset_pi P) (product_isProjective P)

instance (P : ∀ i, Measure (α i)) [∀ i, IsProbabilityMeasure (P i)] :
    IsProbabilityMeasure (independentFamily' P) := by
  rw [independentFamily']
  infer_instance

noncomputable
def Bernoulli_half : Measure ℝ :=
  ((1 : ℝ≥0) / 2) • Measure.dirac 0 + ((1 : ℝ≥0) / 2) • Measure.dirac 1

instance : IsProbabilityMeasure Bernoulli_half := by
  constructor
  simp only [Bernoulli_half, Measure.add_toOuterMeasure, Measure.smul_toOuterMeasure,
    OuterMeasure.coe_add, OuterMeasure.coe_smul, Pi.add_apply, Pi.smul_apply, MeasurableSet.univ,
    Measure.dirac_apply', Set.mem_univ, Set.indicator_of_mem, Pi.one_apply]
  simp only [ENNReal.smul_def, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
    ENNReal.coe_div, ENNReal.coe_ofNat, smul_eq_mul, mul_one]
  rw [ENNReal.add_halves]
  simp only [ENNReal.coe_one]

noncomputable
def NBernoulli_half : Measure (ℕ → ℝ) := independentFamily' (fun _ ↦ Bernoulli_half)

instance: IsProbabilityMeasure NBernoulli_half := by
  rw [NBernoulli_half]
  infer_instance

I am very slowly merging the code of the repository into Mathlib. It's slow because I am refactoring it as I go and because I don't have much time for lean now.