Random products in compact groups

DefinitionFair coin measure#✓fully proved

The fair coin measure is the measure \(\tfrac12 \delta_{\mathrm{false}} + \tfrac12 \delta_{\mathrm{true}}\) on the Booleans \(\{\mathrm{false}, \mathrm{true}\}\): it gives mass \(1/2\) to each of the two values.

noncomputable def coinFlip : MeasureTheory.Measure Bool :=
  (1 / 2 : ℝ≥0∞) • MeasureTheory.Measure.dirac false +
    (1 / 2 : ℝ≥0∞) • MeasureTheory.Measure.dirac true

Used by 1

Used byFair coin product measure

DefinitionFair coin product measure#✓fully proved

The fair coin product measure is the measure on the space of Boolean sequences \(c : \mathbb{N} \to \{\mathrm{false}, \mathrm{true}\}\) given by the infinite product, over \(n \in \mathbb{N}\), of the fair coin measure, which gives mass \(1/2\) to each of \(\mathrm{false}\) and \(\mathrm{true}\).

noncomputable def coinMeasure : MeasureTheory.Measure (ℕ → Bool) :=
  MeasureTheory.Measure.infinitePi fun _ : ℕ => coinFlip

Uses 1 · Used by 1

Statement usesFair coin measure

Used byScottish Book Problem 116(b), measurable-set form

DefinitionGenerator chosen by a coin sequence#✓fully proved

Let \(\varphi\) and \(\psi\) be elements of a type \(G\) and let \(c : \mathbb{N} \to \{\mathrm{false}, \mathrm{true}\}\) be a sequence. For \(n \in \mathbb{N}\), the \(n\)-th chosen generator is \(\varphi\) if \(c(n) = \mathrm{false}\) and \(\psi\) if \(c(n) = \mathrm{true}\).

Index \(0\) corresponds to \(f_1\) in the Scottish Book typescript.

def step {G : Type*} (phi psi : G) (c : ℕ → Bool) (n : ℕ) : G :=
  if c n then psi else phi

Used by 1

Used bySuccessive products along a coin sequence

DefinitionSuccessive products along a coin sequence#✓fully proved

Let \(G\) be a group, let \(\varphi, \psi \in G\), and let \(c : \mathbb{N} \to \{\mathrm{false}, \mathrm{true}\}\). For \(i \ge 1\) let \(f_i\) be the generator chosen at index \(i - 1\): \(f_i = \varphi\) if \(c(i - 1) = \mathrm{false}\) and \(f_i = \psi\) if \(c(i - 1) = \mathrm{true}\). The successive products are defined by \(P_0 = 1\) and \(P_{n+1} = P_n f_{n+1}\), so \(P_n = f_1 f_2 \cdots f_n\) for every \(n \in \mathbb{N}\), with \(P_0\) the empty product.

The typescript writes the terms as \(f_1, f_1(f_2), f_1(f_2 f_3), \ldots\), read as successive products.

def partialProd {G : Type*} [Group G] (phi psi : G) (c : ℕ → Bool) : ℕ → G
  | 0 => 1
  | n + 1 => partialProd phi psi c n * step phi psi c n

Uses 1 · Used by 1

Statement usesGenerator chosen by a coin sequence

Used byScottish Book Problem 116(b), measurable-set form

DefinitionScottish Book Problem 116(b), measurable-set form#✓fully proved

The claim is the following. Let \(G\) be any compact Hausdorff topological group with its Borel \(\sigma\)-algebra, and let \(\mu\) be a Haar measure on \(G\) that is a probability measure. For \(\varphi, \psi \in G\) and a Boolean sequence \(c : \mathbb{N} \to \{\mathrm{false}, \mathrm{true}\}\), let \(f_{n+1} = \varphi\) if \(c(n) = \mathrm{false}\) and \(f_{n+1} = \psi\) if \(c(n) = \mathrm{true}\), and define the successive products by \(P_0 = 1\) and \(P_{n+1} = P_n f_{n+1}\). Then for \((\mu \otimes \mu)\)-almost every pair \((\varphi, \psi) \in G \times G\), if the subgroup generated by \(\varphi\) and \(\psi\) is dense in \(G\), then for almost every \(c\) with respect to the fair coin product measure, for every measurable set \(V \subseteq G\),

\[\lim_{N \to \infty} \frac{\#\{n < N : P_n \in V\}}{N} = \mu(V).\]

The typescript's "region" is read as an arbitrary measurable set, since the typescript does not specify a class of regions; the set \(V\) is quantified after \(c\) and may depend on it.

def ScottishBookProblem116bClaim : Prop :=
  ∀ (G : Type*) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [MeasurableSpace G] [BorelSpace G]
    (μ : MeasureTheory.Measure G)
    [MeasureTheory.Measure.IsHaarMeasure μ] [MeasureTheory.IsProbabilityMeasure μ],
    ∀ᵐ p ∂(μ.prod μ),
      Dense ((Subgroup.closure {p.1, p.2} : Subgroup G) : Set G) →
        ∀ᵐ c ∂coinMeasure,
          ∀ V : Set G, MeasurableSet V →
        Filter.Tendsto
          (fun N : ℕ =>
            ((@Finset.filter ℕ (fun n => partialProd p.1 p.2 c n ∈ V)
              (fun _n => Classical.propDecidable _) (Finset.range N)).card : ℝ) / (N : ℝ))
          Filter.atTop (𝓝 (μ V).toReal)

Uses 2 · Used by 1

Statement usesFair coin product measure · Successive products along a coin sequence

Used byScottish Book Problem 116(b) fails for arbitrary measurable sets

TheoremScottish Book Problem 116(b) fails for arbitrary measurable sets#●ready to prove

The measurable-set form of Scottish Book Problem 116(b) is false. For \(\varphi, \psi\) in a group \(G\) and a Boolean sequence \(c : \mathbb{N} \to \{\mathrm{false}, \mathrm{true}\}\), let \(f_{n+1} = \varphi\) if \(c(n) = \mathrm{false}\) and \(f_{n+1} = \psi\) if \(c(n) = \mathrm{true}\), and define the successive products by \(P_0 = 1\) and \(P_{n+1} = P_n f_{n+1}\). It is not the case that for every compact Hausdorff topological group \(G\) with its Borel \(\sigma\)-algebra and Haar probability measure \(\mu\), for \((\mu \otimes \mu)\)-almost every pair \((\varphi, \psi) \in G \times G\) generating a dense subgroup of \(G\), for almost every \(c\) under the fair coin product measure and every measurable set \(V \subseteq G\), the proportion of \(P_0, \ldots, P_{N-1}\) that lie in \(V\) tends to \(\mu(V)\) as \(N \to \infty\).

Counterexample: take \(G\) to be the circle \(S^1\) with normalized Lebesgue measure. Almost every pair \((\varphi, \psi)\) generates a dense subgroup. For any such pair and any \(c\), the set \(V_c\) of all successive products is countable, hence measurable with \(\mu(V_c) = 0\), yet every successive product lies in \(V_c\), so the proportion equals \(1\) for every \(N \ge 1\). The set \(V\) may depend on \(c\) because it is quantified after \(c\), and the only condition on \(V\) is measurability. The version restricted to sets \(V\) whose frontier has measure \(0\) is a different statement, filed separately in OpenConjectures.

theorem_wanted scottishBook116b_refuted : ¬ ScottishBookProblem116bClaim

Sources

• J. Schreier and S. Ulam, Problem 116, part (b) of the Scottish Book, typescript PDF p. 56, printed p. 53; see the commentary in R. D. Mauldin (ed.), The Scottish Book, 2nd ed. (Birkhäuser, 2015).

Uses 1

Statement usesScottish Book Problem 116(b), measurable-set form

5 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.