Projective limits on countable products

This file extends the sequence-indexed Kolmogorov extension theorem from TauCeti.MeasureTheory.Measure.ProjectiveLimit.Nat to an arbitrary countable index type. Finite index types are handled directly by the law on all coordinates; infinite countable types are enumerated and reduced to the sequence theorem.

Main result

• TauCeti.Measure.exists_isProjectiveLimit_of_countable realizes every projective family of probability laws on finite subsets of a countable family of standard Borel spaces.

The proof transports finite-dimensional laws along measurable equivalences of dependent products. This is the arbitrary-countable-index existence bridge required by TauCetiRoadmap/OptimalTransport/README.md, Layer 0, item 4.

theorem TauCeti.Measure.exists_isProjectiveLimit_of_countable {ι : Type u} {X : ι → Type u_1} [(i : ι) → MeasurableSpace (X i)] [Countable ι] [∀ (i : ι), StandardBorelSpace (X i)] (P : (I : Finset ι) → MeasureTheory.Measure ((i : ↥I) → X ↑i)) [∀ (I : Finset ι), MeasureTheory.IsProbabilityMeasure (P I)] (hP : MeasureTheory.IsProjectiveMeasureFamily P) : ∃ (μ : MeasureTheory.Measure ((i : ι) → X i)), MeasureTheory.IsProbabilityMeasure μ ∧ MeasureTheory.IsProjectiveLimit μ P

Kolmogorov extension on an arbitrary countable index type. Every projective family of probability laws on the finite subproducts of a countable family of standard Borel spaces has a projective limit, which is again a probability measure.

For finite index types the full-dimensional member of the family is already the desired law. For infinite countable types, an enumeration reduces the result to TauCeti.Measure.exists_isProjectiveLimit_nat. Mathlib's MeasureTheory.IsProjectiveLimit.unique gives uniqueness.