The path law of a mixed i.i.d. process

A mixed i.i.d. process has, as its path law, a mixture of infinite product measures: for a mixing representative ν,

pathLaw μ X = ∫ P^{⊗ℕ} d(μ.map ν)(P)

written in the Measure.bind idiom.

Main results

• pathLaw_eq_bind_infinitePi_of_mixedIIDWith — the representation, for an arbitrary mixing representative.
• mixedIID_mixingLaw_eq_of_pathLaw_eq — the mixing law is a function of the path law alone.
• mixedIID_mixingLaw_unique — the mixing law μ.map ν is determined by the process.
• MixedIID.existsUnique_mixingLaw — a mixed i.i.d. process under a probability law has a unique probability mixing law in the infinite-product representation.

The witness-level representation and uniqueness results need only [IsFiniteMeasure μ], a.e.-measurable coordinates, and the witness. MixedIID.existsUnique_mixingLaw assumes [IsProbabilityMeasure μ] only so that the unique mixing law can be bundled as a ProbabilityMeasure. No standard-Borel hypothesis appears: that is the cost of supplying a canonical witness, not of using one, so this file carries no de Finetti dependency.

Implementation

MixedIIDWith constrains only the finite blocks, so the work is the passage from finite blocks to the whole path. The two sides are compared through their finite-dimensional prefix marginals via measure_eq_of_prefixProj_map_eq: on the left map_prefixProj_pathLaw and the block identity, on the right map_bind to push the marginal inside the mixture, map_prefixProj_infinitePi_const to recognise each prefix marginal of an infinite power as the corresponding finite power, and bind_map to re-index the mixture over μ rather than over μ.map ν.

This advances TauCetiRoadmap/Exchangeability/README.md, Layer 6, the directing-measure API bullet asking for the mixture-of-product-measures form. That bullet also asks for π to be the unique law of ν, which mixedIID_mixingLaw_unique now supplies: the mixture representation turns two witnesses into the same Measure.bind, and injectivity of π ↦ π.bind (P ↦ P^{⊗ℕ}) (Measure.ext_of_bind_infinitePi_eq) identifies the mixing laws. The roadmap name deFinetti_mixture, which derives the unique representation from exchangeability rather than assuming a witness, lives in TauCeti.Probability.DeFinetti.Representation.

theorem TauCeti.Probability.pathLaw_eq_bind_infinitePi_of_mixedIIDWith {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} (h : MixedIIDWith μ X ν) : pathLaw μ X = (MeasureTheory.Measure.map ν μ).bind fun (P : MeasureTheory.ProbabilityMeasure α) => MeasureTheory.Measure.infinitePi fun (x : ℕ) => ↑P

The mixture representation of a path law. If ν is a mixing representative for X, the path law of X is the μ.map ν-mixture of the infinite product measures P^{⊗ℕ}.

theorem TauCeti.Probability.mixedIID_mixingLaw_eq_of_pathLaw_eq {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {Ω' : Type u_3} [MeasurableSpace Ω'] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {μ' : MeasureTheory.Measure Ω'} [MeasureTheory.IsFiniteMeasure μ'] {X : ℕ → Ω → α} {Y : ℕ → Ω' → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} {ν' : Ω' → MeasureTheory.ProbabilityMeasure α} (h : MixedIIDWith μ X ν) (h' : MixedIIDWith μ' Y ν') (hpath : pathLaw μ X = pathLaw μ' Y) : MeasureTheory.Measure.map ν μ = MeasureTheory.Measure.map ν' μ'

The mixing law is a function of the path law. Two mixed i.i.d. processes with the same path law — on possibly different sample spaces — have mixing representatives with the same law.

This is the sharp form of mixing-law uniqueness: the mixture representation writes the path law as π.bind (P ↦ P^{⊗ℕ}) for π = μ.map ν, and that assignment is injective (Measure.ext_of_bind_infinitePi_eq), so the path law already determines π. Comparing two witnesses for one and the same process (mixedIID_mixingLaw_unique) is the special case hpath = rfl.

theorem TauCeti.Probability.mixedIID_mixingLaw_unique {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} {ν ν' : Ω → MeasureTheory.ProbabilityMeasure α} (h : MixedIIDWith μ X ν) (h' : MixedIIDWith μ X ν') : MeasureTheory.Measure.map ν μ = MeasureTheory.Measure.map ν' μ

Uniqueness of the mixing law. Two mixing representatives for the same process induce the same law on ProbabilityMeasure α.

Only the law μ.map ν is unique, not the witness. For a nondegenerate mixing law an independent copy of a mixing representative is another one, so no witness-level a.e.-equality theorem can conclude ν =ᵐ[μ] ν' from MixedIIDWith alone; a.e. uniqueness of the witness belongs to the conditional predicate (conditionallyIID_ae_unique).

Finiteness of μ is load-bearing rather than decorative: for an infinite base measure, distinct mixing measures can produce identical ∞-valued finite-dimensional mixtures, so mixing-law uniqueness fails at the hypothesis-light generality the definitions otherwise enjoy.

Normalization, however, is not needed. The roadmap states this target with [IsProbabilityMeasure μ], but the justification it gives only separates finite from infinite base measures, and the proof goes through for any finite μ.

theorem TauCeti.Probability.MixedIID.existsUnique_mixingLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → α} (h : MixedIID μ X) : ∃! π : MeasureTheory.ProbabilityMeasure (MeasureTheory.ProbabilityMeasure α), pathLaw μ X = (↑π).bind fun (P : MeasureTheory.ProbabilityMeasure α) => MeasureTheory.Measure.infinitePi fun (x : ℕ) => ↑P

Existence and uniqueness of the mixing law. A mixed i.i.d. process under a probability law has a unique probability measure π on ProbabilityMeasure α such that its path law is the π-mixture of the infinite product measures P^{⊗ℕ}.

This identifies the mixing law intrinsically from the path law, rather than merely comparing the pushforwards of two supplied mixing representatives as mixedIID_mixingLaw_unique does.