The canonical i.i.d. trial process, over an arbitrary law

Category: 1-Mathlib (CSD-free upstream candidate).

LF4/TrialWitness.lean built the canonical i.i.d. process for the Fubini–Study law on ℂℙ^{N−1} (fsTrialSpace / fsTrialMeasure / fsTrial, with its law and independence lemmas). Nothing in that construction is specific to either the space or the measure: it is Measure.infinitePi of a constant family, evaluation as the trial, and the standard independence of coordinates.

The fibred arena needs the same thing for epistemicMeasure on KSigma N, which is the second consumer — so by CONVENTIONS §9 (rule of two) the construction is extracted here rather than copied.

What is provided

For any measurable space X and probability measure μ:

• iidSpace X — the trial space ℕ → X;
• iidMeasure μ — the i.i.d. law, Measure.infinitePi (fun _ => μ);
• iidTrial X n — the n-th trial (evaluation), with iidTrial_measurable;
• iidTrial_law — each trial has law μ, the hlaw hypothesis of the frequency theorems;
• iidTrial_iIndepFun and iidTrial_pairwise_indepFun_indicator — the hindep hypothesis.

Those five are exactly the inputs born_frequency_convergence_partition asks for, so any frequency theorem stated over an arbitrary law can be instantiated on the canonical process by supplying them.

⚠️ LF4/TrialWitness.lean's fsTrial* block is now a fold candidate: it is this construction at μ := fsMeasure p₀. It is left in place because it has live consumers whose statements name it, and re-pointing them is churn without benefit; the duplication is recorded here rather than left for someone to rediscover.

References

LF4/TrialWitness.lean (fsTrialSpace, fsTrialMeasure, fsTrial, and the twins of every lemma below); LF4/BornFrequencyPartition.lean (born_frequency_convergence_partition, whose hypotheses these supply); RecordLayer/BasinFrequency.lean (the second consumer); CONVENTIONS.md §9.

@[reducible, inline]

abbrev MeasureTheory.iidSpace (X : Type u_2) : Type u_2

The canonical trial space: one draw per natural number.

Equations

• MeasureTheory.iidSpace X = (ℕ → X)

noncomputable def MeasureTheory.iidMeasure {X : Type u_1} [MeasurableSpace X] (μ : Measure X) : Measure (iidSpace X)

The canonical i.i.d. law with marginal μ.

Equations

• MeasureTheory.iidMeasure μ = MeasureTheory.Measure.infinitePi fun (x : ℕ) => μ

instance MeasureTheory.instIsProbabilityMeasureIidMeasure {X : Type u_1} [MeasurableSpace X] (μ : Measure X) [IsProbabilityMeasure μ] : IsProbabilityMeasure (iidMeasure μ)

def MeasureTheory.iidTrial (X : Type u_2) (n : ℕ) : iidSpace X → X

The n-th canonical trial.

Equations

• MeasureTheory.iidTrial X n ω = ω n

theorem MeasureTheory.iidTrial_measurable {X : Type u_1} [MeasurableSpace X] (n : ℕ) : Measurable (iidTrial X n)

Each canonical trial is measurable — the hX hypothesis.

theorem MeasureTheory.iidTrial_law {X : Type u_1} [MeasurableSpace X] (μ : Measure X) [IsProbabilityMeasure μ] (n : ℕ) : Measure.map (iidTrial X n) (iidMeasure μ) = μ

Each canonical trial has law μ — the hlaw hypothesis.

theorem MeasureTheory.iidTrial_iIndepFun {X : Type u_1} [MeasurableSpace X] (μ : Measure X) [IsProbabilityMeasure μ] : ProbabilityTheory.iIndepFun (iidTrial X) (iidMeasure μ)

The canonical trials are jointly independent.

theorem MeasureTheory.iidTrial_pairwise_indepFun_indicator {X : Type u_1} [MeasurableSpace X] (μ : Measure X) [IsProbabilityMeasure μ] {ι : Type u_2} (S : ι → Set X) (hS : ∀ (i : ι), MeasurableSet (S i)) (i : ι) : Pairwise (Function.onFun (fun (f g : iidSpace X → ℝ) => ProbabilityTheory.IndepFun f g (iidMeasure μ)) fun (n : ℕ) => (iidTrial X n ⁻¹' S i).indicator fun (x : iidSpace X) => 1)

Indicators of a fixed event across trials are pairwise independent — the hindep hypothesis of the frequency theorems, in the shape they ask for.