The conditional strong law of large numbers

A conditionally i.i.d. process obeys the strong law of large numbers conditionally: almost surely, the averages of a bounded observable along the process converge to that observable's integral against the directing measure, not against a deterministic law. Taking the observable to be an indicator: for each fixed measurable set, the empirical frequency of that set converges almost surely to the mass the directing measure gives it.

ConditionallyIID/EmpiricalMeasure.lean already gives the L² form of this, with the exact finite-sample error. What is new here is almost-sure convergence, and the strengthening from a single measurable set to a countable family of sets under one null set.

The quantifier order matters, and ∀ B, ∀ᵐ ω is the strongest order available here: the null set genuinely depends on the set tested. Setwise almost-sure convergence — one null set outside which the empirical measures converge on every measurable set at once — is false as soon as the directing measure is nonatomic, since the countable range of the sample path then carries empirical mass 1 and directing mass 0. Countability is exactly the room there is to improve the order, and tendsto_empiricalMeasure_apply_ae_forall takes all of it.

Main results

• ConditionallyIIDWith.tendsto_average_ae — the conditional strong law for a bounded measurable observable valued in a Banach space;
• ConditionallyIIDWith.tendsto_integral_empiricalMeasure_ae — its reading through empiricalMeasure;
• ConditionallyIIDWith.tendsto_empiricalMeasure_apply_ae and ConditionallyIIDWith.tendsto_empiricalMeasure_apply_ae_forall — the empirical frequencies, for one fixed measurable set and for a countable family of them under a single null set;

The de Finetti endpoint of these — the same statement for an exchangeable process, where the directing measure has to be produced first — is deFinetti_tendsto_empiricalMeasure_apply in DeFinetti/EmpiricalMeasure.lean. It is kept out of this module so that the conditional strong law does not drag the de Finetti summit into every importer's closure.

Implementation

The conditional statement is reduced to an unconditional one by the full-path joint disintegration ConditionallyIIDWith.jointPathLaw_eq_iidMixtureLaw: the law of the pair (ν, X) on ProbabilityMeasure α × (ℕ → α) is the mixture ∫ δ_Q ⊗ Q^{⊗ℕ} d(μ.map ν)(Q). The event

G = {(Q, x) | the averages of `f` along `x` converge to `∫ f dQ`}

is measurable — measurableSet_tendsto_fun, using that Q ↦ ∫ f dQ is measurable, which is Mathlib's MeasureTheory.StronglyMeasurable.integral_kernel for the coercion kernel ProbabilityMeasure α → Measure α — and every fibre δ_Q ⊗ Q^{⊗ℕ} of the mixture puts full mass on it, which is exactly strong_law_ae_infinitePi at the law Q. Mixing over Q and transporting the resulting almost-sure statement back along ω ↦ (ν ω, X · ω) gives the conditional strong law. No martingale or ergodic input is used: the joint disintegration already carries all the conditional structure, and Mathlib's strong law does the analysis.

Boundedness of the observable is what makes the argument uniform in Q: it gives integrability against every probability measure at once, and it is all the empirical-measure corollaries need.

References

• Roadmap: TauCetiRoadmap/Exchangeability/README.md, Layer 6's empirical form of the directing-measure theorem. This module supplies the topology-free fixed-set core; weak empirical-measure convergence is the separate downstream theorem ConditionallyIIDWith.tendsto_empiricalMeasure_ae in ConditionallyIID/WeakConvergence.lean, which needs only a second-countable topology on α whose open sets are measurable. It tests against a countable determining class, and tendsto_empiricalMeasure_apply_ae_forall is the "one null set for a countable determining class" step it consumes.
• O. Kallenberg, Probabilistic Symmetries and Invariance Principles (Springer, 2005), §1.1.

No material is adapted from cameronfreer/exchangeability, which does not treat empirical measures.

theorem TauCeti.Probability.ConditionallyIIDWith.tendsto_average_ae {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [MeasureTheory.IsFiniteMeasure μ] (h : ConditionallyIIDWith μ X ν) {f : α → E} (hf : Measurable f) {C : ℝ} (hbdd : ∀ (x : α), ‖f x‖ ≤ C) : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ • ∑ i ∈ Finset.range n, f (X i ω)) Filter.atTop (nhds (∫ (y : α), f y ∂↑(ν ω)))

The conditional strong law of large numbers. For a conditionally i.i.d. process and a bounded measurable observable f valued in a Banach space, the averages of f along the process converge almost surely to the integral of f against the directing measure.

The limit is random: it is ∫ f dν(ω). It reduces to a constant when the directing measure is almost everywhere constant, but also for observables — f = 0, say — whose integral happens not to see the randomness of ν.

theorem TauCeti.Probability.ConditionallyIIDWith.tendsto_integral_empiricalMeasure_ae {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} [MeasureTheory.IsFiniteMeasure μ] (h : ConditionallyIIDWith μ X ν) {f : α → ℝ} (hf : Measurable f) {C : ℝ} (hbdd : ∀ (x : α), |f x| ≤ C) : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => ∫ (y : α), f y ∂↑(empiricalMeasure (fun (i : ℕ) => X i ω) n)) Filter.atTop (nhds (∫ (y : α), f y ∂↑(ν ω)))

The conditional strong law, read through empirical measures. The integral of a bounded measurable observable against the empirical measure of a conditionally i.i.d. process converges almost surely to its integral against the directing measure.

theorem TauCeti.Probability.ConditionallyIIDWith.tendsto_empiricalMeasure_apply_ae {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} [MeasureTheory.IsFiniteMeasure μ] (h : ConditionallyIIDWith μ X ν) {B : Set α} (hB : MeasurableSet B) : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑(empiricalMeasure (fun (i : ℕ) => X i ω) n) B).toReal) Filter.atTop (nhds (↑(ν ω) B).toReal)

Empirical frequencies converge almost surely, on each fixed measurable set. For a conditionally i.i.d. process and a fixed measurable set B, the empirical frequency of B converges almost surely to the mass the directing measure gives it.

The null set depends on B, and outside a countable family of sets it must: tendsto_empiricalMeasure_apply_ae_forall is as far as the quantifiers can be interchanged.

The L² form of the same convergence is ConditionallyIIDWith.tendsto_integral_empiricalMeasure_apply_sub_sq, and ConditionallyIIDWith.integral_empiricalMeasure_apply_sub_sq computes its exact finite-sample error.

theorem TauCeti.Probability.ConditionallyIIDWith.tendsto_empiricalMeasure_apply_ae_forall {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} [MeasureTheory.IsFiniteMeasure μ] {ι : Type u_4} [Countable ι] (h : ConditionallyIIDWith μ X ν) {B : ι → Set α} (hB : ∀ (j : ι), MeasurableSet (B j)) : ∀ᵐ (ω : Ω) ∂μ, ∀ (j : ι), Filter.Tendsto (fun (n : ℕ) => (↑(empiricalMeasure (fun (i : ℕ) => X i ω) n) (B j)).toReal) Filter.atTop (nhds (↑(ν ω) (B j)).toReal)

A single null set serves a countable family of sets. Almost surely, the empirical frequencies of every member of a countable family of measurable sets converge simultaneously.

Interchanging the two quantifiers is not cosmetic: an upgrade of setwise convergence to convergence in the weak topology on ProbabilityMeasure α tests against a countable determining class, and needs the null set to be chosen before the class is inspected.