Almost sure uniqueness of the directing measure

A directing measure — a witness of ConditionallyIIDWith μ X ν — is pinned down almost everywhere: any two of them agree μ-a.e. This is the sharp uniqueness statement that the mixture predicate MixedIIDWith fails to have, where only the mixing law μ.map ν is unique (mixedIID_mixingLaw_unique); an independent copy of a directing measure is another mixing representative but not another directing measure.

Main results

• conditionallyIID_ae_unique — two directing measures of the same process are a.e. equal.
• ConditionallyIIDWith.ae_measure_apply_eq — the setwise form it is promoted from: on each fixed measurable set the two directing masses agree a.e.

The L² estimates driving both come from ConditionallyIID/Moments.lean; this file consumes them and does no moment computation of its own.

Implementation

The directing measure is recovered from the process by a law of large numbers, and the joint-law form of ConditionallyIIDWith gives the second-moment version of that law directly, with no conditional expectations. Writing q ω = (ν ω) B and eᵢ for the indicator of Xᵢ ∈ B, the weighted block identity supplies the three moments

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

the last of which is the genuinely conditional input: it is the joint law of (ν, Xᵢ), not the marginal law of Xᵢ, that the mixture predicate would leave free. The centred variables eᵢ - q are therefore uncorrelated with common variance ∫ q - ∫ q², so the averages of eᵢ converge to q with mean square error O(1/n), hence in L² at rate O(1/√n). Both directing measures are approximated by the same averages, so the triangle inequality forces ∫ (q - q')² = 0 for every measurable B, and a countable generating set algebra promotes that to a.e. equality of the random measures themselves.

The hypothesis [MeasurableSpace.CountablyGenerated α] is what the final promotion needs, and is all it needs: no measure on α is constructed here, so no standard-Borel or non-empty structure is required.

Coordinatewise a.e. measurability is not assumed: it comes from the ConditionallyIIDWith witness through ConditionallyIIDWith.aemeasurable. A.e. measurability is all that is ever needed, as elsewhere in the measure-theoretic exchangeability API, since every statement here sees X through integrals and hence only modulo μ-a.e. equality.

Uniqueness

theorem TauCeti.Probability.ConditionallyIIDWith.ae_measure_apply_eq {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν ν' : Ω → MeasureTheory.ProbabilityMeasure α} {B : Set α} [MeasureTheory.IsProbabilityMeasure μ] (h : ConditionallyIIDWith μ X ν) (h' : ConditionallyIIDWith μ X ν') (hB : MeasurableSet B) : (fun (ω : Ω) => ↑(ν ω) B) =ᵐ[μ] fun (ω : Ω) => ↑(ν' ω) B

Two directing measures of the same process assign the same mass to each fixed measurable set, almost everywhere.

Both are approximated in L² by the same empirical frequencies, at a rate that does not depend on the witness, so the triangle inequality forces their difference to vanish in L².

theorem TauCeti.Probability.conditionallyIID_ae_unique {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν ν' : Ω → MeasureTheory.ProbabilityMeasure α} [MeasureTheory.IsProbabilityMeasure μ] [MeasurableSpace.CountablyGenerated α] (h : ConditionallyIIDWith μ X ν) (h' : ConditionallyIIDWith μ X ν') : ν =ᵐ[μ] ν'

The directing measure is almost surely unique. Two witnesses of ConditionallyIIDWith for the same process agree almost everywhere.

This is the uniqueness statement that belongs to the conditional predicate. Its mixture analogue is false at the level of witnesses: for a nondegenerate mixing law an independent copy of a directing measure is another mixing representative, and only the mixing law μ.map ν is determined (mixedIID_mixingLaw_unique).

[MeasurableSpace.CountablyGenerated α] is the whole requirement on α: the proof compares two directing measures on a countable generating algebra and never constructs a measure, so neither standard-Borel structure nor non-emptiness is needed.