The mixing measure is identified by the i.i.d. mixture

The map π ↦ π.bind (P ↦ P^{⊗ℕ}), sending a measure on ProbabilityMeasure α to the law of a sequence drawn i.i.d. from a π-random probability measure, is injective on finite measures.

Main results

• Measure.ext_of_bind_infinitePi_eq — two finite measures on ProbabilityMeasure α inducing the same mixture are equal.

Sources

The construction and proof plan follow the human-authored roadmap TauCetiRoadmap/Exchangeability/README.md, Layer 6 — directing measures and de Finetti representation, which names mixing-law uniqueness as the target this theorem serves.

Implementation

Evaluating the mixture on a finite-dimensional rectangle gives the mixed moment ∫⁻ P, ∏ i, P (B i) ∂π of the evaluation maps. Nothing forces the sets B i to be distinct, so listing B j exactly m j times turns the rectangle identity into one for the mixed monomial ∏ j, (P (B j)) ^ m j — this is the whole of the passage from rectangles to moments, and it is where the argument gains its strength.

From there the two imported ingredients finish it. A finite evaluation family takes values in the compact box [0,1]^k, so Measure.ext_of_forall_integral_monomial_eq_of_support identifies its law from those monomials; and Measure.ext_of_forall_map_probabilityMeasure_eval_eq promotes agreement of every finite evaluation law to equality of the measures.

Only π₁ is assumed finite. Every infinite product of probability measures is a probability measure, so the mixture has the same total mass as its mixing measure, and equality of the two mixtures transfers finiteness to π₂.

theorem TauCeti.MeasureTheory.Measure.ext_of_bind_infinitePi_eq {α : Type u_1} [MeasurableSpace α] {π₁ π₂ : MeasureTheory.Measure (MeasureTheory.ProbabilityMeasure α)} [MeasureTheory.IsFiniteMeasure π₁] (h : (π₁.bind fun (P : MeasureTheory.ProbabilityMeasure α) => MeasureTheory.Measure.infinitePi fun (x : ℕ) => ↑P) = π₂.bind fun (P : MeasureTheory.ProbabilityMeasure α) => MeasureTheory.Measure.infinitePi fun (x : ℕ) => ↑P) : π₁ = π₂

The i.i.d. mixture determines the mixing measure. If two finite measures on ProbabilityMeasure α induce the same mixture π.bind (P ↦ P^{⊗ℕ}), they are equal.

The mixture's finite-dimensional rectangle probabilities are the mixed moments of the evaluation maps, and repetitions in the rectangle turn those into mixed monomials. Each finite evaluation family lands in the compact box [0,1]^k, so multivariate moment determinacy identifies its law, and finite evaluation laws determine the measure.