The strong law of large numbers on a countable product space

Mathlib's ProbabilityTheory.strong_law_ae takes a sequence of pairwise independent, identically distributed, integrable random variables on an abstract probability space. The canonical carrier of such a sequence is the countable power Measure.infinitePi fun _ : ℕ => Q with its coordinate maps, and this file specializes the strong law to it.

Main results

• TauCeti.Probability.strong_law_ae_infinitePi — for f measurable and integrable against Q, the averages n⁻¹ • ∑_{i < n} f (xᵢ) converge Q^{⊗ℕ}-almost everywhere to ∫ f dQ.

Implementation

Independence of the coordinates is Mathlib's ProbabilityTheory.iIndepFun_infinitePi for the identity variables. Nothing is reproved about product measures.

The strong law itself is then Mathlib's, applied to x ↦ f (x i): the three hypotheses come from that independence and from measurePreserving_eval_infinitePi, which makes the coordinates identically distributed, transports integrability, and identifies the limit 𝔼[f ∘ eval 0] with ∫ f dQ.

f is assumed measurable, not merely almost-everywhere strongly measurable as Integrable f Q gives: it has to be composed with the coordinate maps, so that independence and identical distribution of the coordinates transfer to the summands.

This is general probability theory with no exchangeability in its statements. It is used by the conditional strong law for conditionally i.i.d. processes in TauCeti.Probability.Exchangeability.ConditionallyIID.StrongLaw, where the conditional statement is reduced fibrewise to this one over the mixing law; see TauCetiRoadmap/Exchangeability/README.md, Layer 6 (the empirical-measure form of the directing-measure theorem).

theorem TauCeti.Probability.strong_law_ae_infinitePi {α : Type u_1} [MeasurableSpace α] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] (Q : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure Q] {f : α → E} (hf : Measurable f) (hint : MeasureTheory.Integrable f Q) : ∀ᵐ (x : ℕ → α) ∂MeasureTheory.Measure.infinitePi fun (x : ℕ) => Q, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ • ∑ i ∈ Finset.range n, f (x i)) Filter.atTop (nhds (∫ (y : α), f y ∂Q))

The strong law of large numbers on the canonical i.i.d. model. For an f that is measurable and integrable against Q, the averages of f along the coordinates of Q^{⊗ℕ} converge almost everywhere to ∫ f dQ.

This is Mathlib's ProbabilityTheory.strong_law_ae for the coordinate process of a countable power; it is the form in which a statement about some i.i.d. sequence becomes a statement about the product measure itself, and so can be integrated over a mixing law.