Conditional moment identities and the empirical-frequency rate

The second-moment consequences of the joint-law disintegration ConditionallyIIDWith, culminating in an exact finite-sample formula for the integrated squared error of an empirical frequency.

Main results

• ConditionallyIIDWith.lintegral_mul_indicator_iInter — the weighted block identity: testing the disintegration against g (ν ω) times the indicator of a block rectangle turns the block into the power (ν ω) B ^ m. Its one- and two-coordinate specializations are ConditionallyIIDWith.lintegral_mul_indicator_single and ConditionallyIIDWith.lintegral_mul_indicator_pair.
• ConditionallyIIDWith.integral_empiricalFrequency_sub_sq — the exact rate: for the empirical frequency of a measurable set B along the first n coordinates, the integral of its squared deviation from (ν ·) B is exactly (∫ (ν ·) B - ∫ ((ν ·) B) ^ 2) / n. At a probability measure this reads as the mean square error, with an averaged Bernoulli variance on the right.
• ConditionallyIIDWith.integral_empiricalFrequency_sub_sq_le — its ≤ 1 / n corollary, and the only statement here that needs μ univ = 1.
• ConditionallyIIDWith.tendsto_integral_empiricalFrequency_sub_sq — the limit the identity gives: fixed-set empirical frequencies converge to (ν ·) B in L².

Implementation

The joint-law form of ConditionallyIIDWith gives the second moments directly, with no conditional expectations. Writing q ω = (ν ω) B and eᵢ for the indicator of Xᵢ ∈ B, the weighted block identity supplies

∫ eᵢ = ∫ q,      ∫ eᵢ eⱼ = ∫ q²  (i ≠ j),      ∫ q eᵢ = ∫ q²,

the last of which is the genuinely conditional input: it constrains the joint law of (ν, Xᵢ), which the mixture predicate MixedIIDWith would leave free. The centred variables eᵢ - q therefore integrate against each other to ∫ q - ∫ q² on the diagonal and to 0 off it, which is exactly the stated rate; at a probability measure that reads as uncorrelated with common variance ∫ q - ∫ q².

The identities are stated in ℝ≥0∞ first, where the disintegration lives, and converted to Bochner integrals by the private machinery below. Coordinatewise a.e. measurability is not assumed: it is supplied by the ConditionallyIIDWith witness through ConditionallyIIDWith.aemeasurable, and a.e. measurability is all that is ever needed, as elsewhere in the measure-theoretic exchangeability API.

These estimates are consumed by ConditionallyIID.Unique for a.e. uniqueness of the directing measure.

The O(1/n) rate is not summable, so it gives L² convergence but not almost-sure convergence; the latter needs a different argument. Convergence on a countable determining class, empirical probability measures as objects, and weak convergence — which additionally requires a chosen Polish topology, since StandardBorelSpace α asserts only that some compatible topology exists — are all separate developments.

Weighted block identities

theorem TauCeti.Probability.ConditionallyIIDWith.lintegral_mul_indicator_iInter {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} {B : Set α} (h : ConditionallyIIDWith μ X ν) {m : ℕ} {k : Fin m → ℕ} (hk : Function.Injective k) {g : MeasureTheory.ProbabilityMeasure α → ENNReal} (hg : Measurable g) (hB : MeasurableSet B) : ∫⁻ (ω : Ω), g (ν ω) * (⋂ (i : Fin m), X (k i) ⁻¹' B).indicator 1 ω ∂μ = ∫⁻ (ω : Ω), g (ν ω) * ↑(ν ω) B ^ m ∂μ

The weighted block identity. Integrating the joint-law disintegration of ConditionallyIIDWith against a weight g (ν ω) times the indicator of the event that a block of m distinct coordinates lands in B replaces the block by the power (ν ω) B ^ m.

Taking g = 1 recovers the block probabilities that MixedIIDWith already determines; the content of the conditional predicate is that an arbitrary weight in the directing measure may be carried along.

theorem TauCeti.Probability.ConditionallyIIDWith.lintegral_mul_indicator_single {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} {B : Set α} (h : ConditionallyIIDWith μ X ν) (i : ℕ) {g : MeasureTheory.ProbabilityMeasure α → ENNReal} (hg : Measurable g) (hB : MeasurableSet B) : ∫⁻ (ω : Ω), g (ν ω) * (X i ⁻¹' B).indicator 1 ω ∂μ = ∫⁻ (ω : Ω), g (ν ω) * ↑(ν ω) B ∂μ

One-coordinate form of the weighted block identity.

theorem TauCeti.Probability.ConditionallyIIDWith.lintegral_mul_indicator_pair {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} {B : Set α} (h : ConditionallyIIDWith μ X ν) {i j : ℕ} (hij : i ≠ j) {g : MeasureTheory.ProbabilityMeasure α → ENNReal} (hg : Measurable g) (hB : MeasurableSet B) : ∫⁻ (ω : Ω), g (ν ω) * (X i ⁻¹' B ∩ X j ⁻¹' B).indicator 1 ω ∂μ = ∫⁻ (ω : Ω), g (ν ω) * ↑(ν ω) B ^ 2 ∂μ

Two-coordinate form of the weighted block identity, at distinct indices.

The L² rate for empirical frequencies

theorem TauCeti.Probability.ConditionallyIIDWith.integral_empiricalFrequency_sub_sq {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} {B : Set α} [MeasureTheory.IsFiniteMeasure μ] (h : ConditionallyIIDWith μ X ν) {n : ℕ} (hB : MeasurableSet B) (hn : n ≠ 0) : ∫ (ω : Ω), ((↑n)⁻¹ * ∑ i ∈ Finset.range n, (X i ⁻¹' B).indicator 1 ω - (↑(ν ω) B).toReal) ^ 2 ∂μ = (↑n)⁻¹ * (∫ (ω : Ω), (↑(ν ω) B).toReal ∂μ - ∫ (ω : Ω), (↑(ν ω) B).toReal ^ 2 ∂μ)

The L² rate for empirical frequencies. For a conditionally i.i.d. process with directing measure ν and a measurable set B, the integral of the squared deviation of the empirical frequency of B among the first n coordinates from ω ↦ (ν ω) B is exactly (∫ (ν ·) B - ∫ ((ν ·) B) ^ 2) / n. At a probability measure this is the mean square error and the numerator is the averaged Bernoulli variance of the directing mass; at a general finite measure both sides scale with the total mass.

This is the second-moment law of large numbers for the conditional predicate, read straight off the joint-law disintegration: the cross term ∫ (ν ·) B · 1_{Xᵢ ∈ B} is the one moment that the mixture identity alone does not determine.

theorem TauCeti.Probability.ConditionallyIIDWith.integral_empiricalFrequency_sub_sq_le {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} {B : Set α} [MeasureTheory.IsProbabilityMeasure μ] (h : ConditionallyIIDWith μ X ν) {n : ℕ} (hB : MeasurableSet B) (hn : n ≠ 0) : ∫ (ω : Ω), ((↑n)⁻¹ * ∑ i ∈ Finset.range n, (X i ⁻¹' B).indicator 1 ω - (↑(ν ω) B).toReal) ^ 2 ∂μ ≤ (↑n)⁻¹

The mean square error of ConditionallyIIDWith.integral_empiricalFrequency_sub_sq is at most 1 / n: the factor on the right is a difference of moments of a [0, 1]-valued variable.

Unlike the exact identity above, this bound uses μ univ = 1, so it asks for a probability measure rather than a finite one; at a general finite measure the right-hand side would carry a mass factor.

Convergence of empirical frequencies

theorem TauCeti.Probability.ConditionallyIIDWith.tendsto_integral_empiricalFrequency_sub_sq {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} {B : Set α} [MeasureTheory.IsFiniteMeasure μ] (h : ConditionallyIIDWith μ X ν) (hB : MeasurableSet B) : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω), ((↑(n + 1))⁻¹ * ∑ i ∈ Finset.range (n + 1), (X i ⁻¹' B).indicator 1 ω - (↑(ν ω) B).toReal) ^ 2 ∂μ) Filter.atTop (nhds 0)

Fixed-set empirical frequencies converge in L². For a conditionally i.i.d. process, the empirical frequency of a fixed measurable set B along the first n coordinates converges in L² μ to the directing measure's evaluation (ν ·) B: the integrated squared error tends to 0. At a probability measure this is convergence in mean square.

Indexed at n + 1 so that no caller carries an n ≠ 0 side condition.