Cesàro means of random subsequences

DefinitionFair coin measure#✓fully proved

The fair coin measure is the measure on the Booleans \(\{\mathrm{true}, \mathrm{false}\}\) that gives mass \(1/2\) to each of \(\mathrm{true}\) and \(\mathrm{false}\), that is, \(\frac{1}{2}\delta_{\mathrm{true}} + \frac{1}{2}\delta_{\mathrm{false}}\).

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

Used by 1

Used bySchreier's theorem on Cesàro means of random subsequences

TheoremSchreier's theorem on Cesàro means of random subsequences#●ready to prove

Let \((a_n)_{n \ge 0}\) be a bounded sequence of real numbers whose Cesàro means \(\frac{1}{n} \sum_{i < n} a_i\) converge to a real number \(S\) as \(n \to \infty\). Give the space of Boolean sequences \(\omega = (\omega_n)_{n \ge 0}\) the infinite product of fair coin measures. For such \(\omega\) let \(n_0 < n_1 < \cdots\) list, in increasing order, the indices \(n\) with \(\omega_n = \mathrm{true}\), with \(n_k = 0\) whenever there are at most \(k\) such indices. Then for almost every \(\omega\) the Cesàro means \(\frac{1}{N} \sum_{k < N} a_{n_k}\) of the subsequence \((a_{n_k})\) converge to \(S\) as \(N \to \infty\).

Identifying a subset of \(\mathbb{N}\) with its indicator sequence \(\omega\), this says that almost every subsequence of \((a_n)\) has Cesàro means converging to \(S\).

theorem_wanted schreierCesaroSubsequences :
    ∀ (a : ℕ → ℝ) (S : ℝ), (∃ B : ℝ, ∀ n, |a n| ≤ B) →
      Filter.Tendsto (fun n : ℕ => (∑ i ∈ Finset.range n, a i) / (n : ℝ))
        Filter.atTop (nhds S) →
      ∀ᵐ ω ∂(MeasureTheory.Measure.infinitePi fun _ : ℕ => fairCoinMeasure),
        Filter.Tendsto (fun N : ℕ =>
          (∑ k ∈ Finset.range N, a (Nat.nth (fun n => ω n = true) k)) / (N : ℝ))
          Filter.atTop (nhds S)

Sources

• J. Schreier, Problem 4 of the Scottish Book, stated as a theorem in the Scottish Book typescript.

Uses 1

Statement usesFair coin measure

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.