Mathlib upstream candidate: the canonical i.i.d. coordinate process

For a probability measure μ on α, the coordinate evaluations on the countable product (ι → α, Measure.infinitePi (fun _ => μ)) form a canonical i.i.d. process with common law μ. Mathlib's Measure.infinitePi provides the product measure, Measure.infinitePi_map_eval the marginal law, and ProbabilityTheory.iIndepFun_infinitePi joint independence; this file adds the two glue lemmas a strong-law consumer needs:

• ProbabilityTheory.iIndepFun_eval_infinitePi — the coordinate evaluations of a constant-family infinitePi are jointly independent (the X i = id specialisation of iIndepFun_infinitePi);
• ProbabilityTheory.iIndepFun.pairwise_indepFun_indicator_preimage — from joint independence of a process, the per-trial outcome-region indicators Set.indicator (X n ⁻¹' S i) 1 are pairwise independent, for any family of measurable regions S (composition with the measurable indicator via IndepFun.comp).

Together with Measure.infinitePi_map_eval these inhabit the standard i.i.d.-trial hypothesis bundle (Ω, Pr, X, hX, hlaw, hindep) of SLLN-style frequency theorems.

Category: 1-Mathlib (CSD-free; staged as a Mathlib upstream candidate).

Provenance

Needed for the CSD trial-witness tranche (CsdLean4/LF4/TrialWitness.lean): the volume-frequency capstones (born_frequency_convergence_N_uncond, measurement_flow_born_frequency, …) quantify over an abstract i.i.d. trial bundle; the canonical coordinate process instantiates it, so the capstones' hypothesis sets are Lean-inhabited rather than merely classically satisfiable.

Tags

independence, product measure, iid, indicator, coordinate process

theorem Set.indicator_const_preimage_comp {Ω : Type u_1} {α : Type u_2} {M : Type u_3} [Zero M] (X : Ω → α) (s : Set α) (c : M) : ((X ⁻¹' s).indicator fun (x : Ω) => c) = (s.indicator fun (x : α) => c) ∘ X

The indicator of a preimage X ⁻¹' s with constant value c is the indicator of s composed with X. Function-level form of Set.indicator_comp_right for constant-valued indicators.

theorem ProbabilityTheory.iIndepFun_eval_infinitePi {ι : Type u_1} {α : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] : iIndepFun (fun (n : ι) (ω : ι → α) => ω n) (MeasureTheory.Measure.infinitePi fun (x : ι) => μ)

The coordinate evaluations on a constant-family infinite product Measure.infinitePi (fun _ => μ) are jointly independent. The X i = id specialisation of iIndepFun_infinitePi.

theorem ProbabilityTheory.iIndepFun.pairwise_indepFun_indicator_preimage {Ω : Type u_1} {α : Type u_2} {κ : Type u_3} {ι : Type u_4} {mΩ : MeasurableSpace Ω} [MeasurableSpace α] {Pr : MeasureTheory.Measure Ω} {X : κ → Ω → α} (hXindep : iIndepFun X Pr) (S : ι → Set α) (hS : ∀ (i : ι), MeasurableSet (S i)) (i : ι) : Pairwise (Function.onFun (fun (f g : Ω → ℝ) => IndepFun f g Pr) fun (n : κ) => (X n ⁻¹' S i).indicator fun (x : Ω) => 1)

Indicator independence from joint independence. If the process X is jointly independent, then for every family of measurable outcome regions S : ι → Set α, the per-trial indicators of X n ⁻¹' S i are pairwise independent — the exact hypothesis shape consumed by SLLN-style frequency theorems. No measurability of X is needed: pairwise independence composes with the measurable indicator (IndepFun.comp).