Projective limits on sequences

This file proves a sequence-indexed version of Kolmogorov's extension theorem when every positive-indexed coordinate is standard Borel. Mathlib defines projective measure families and proves uniqueness of their projective limits, while its Ionescu--Tulcea construction produces a path law from a sequence of transition kernels. Here a coherent family of finite-prefix laws is disintegrated to obtain those kernels.

Main result

• TauCeti.Measure.exists_map_frestrictLe_eq constructs a probability measure on a dependent sequence whose finite-prefix laws are a prescribed coherent family.
• TauCeti.Measure.exists_isProjectiveLimit_nat realizes a projective family indexed by finite subsets of ℕ.

This is the existence bridge between Mathlib's MeasureTheory.IsProjectiveMeasureFamily API and its Ionescu--Tulcea theorem. The construction follows the standard proof of Kolmogorov extension for countable products by successive disintegration, as prescribed by the TauCetiRoadmap/OptimalTransport/README.md Layer 0, item 4 target.

theorem TauCeti.Measure.exists_map_frestrictLe_eq {X : ℕ → Type u} [(n : ℕ) → MeasurableSpace (X n)] [∀ (n : ℕ), StandardBorelSpace (X (n + 1))] (P : (n : ℕ) → MeasureTheory.Measure ((i : ↥(Finset.Iic n)) → X ↑i)) [∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (P n)] (hP : ∀ (n : ℕ), MeasureTheory.Measure.map (Preorder.frestrictLe₂ ⋯) (P (n + 1)) = P n) : ∃ (μ : MeasureTheory.Measure ((n : ℕ) → X n)), MeasureTheory.IsProbabilityMeasure μ ∧ ∀ (n : ℕ), MeasureTheory.Measure.map (Preorder.frestrictLe n) μ = P n

Countable projective-family extension for coherent prefixes. A coherent family of probability laws on the prefixes ∀ i : Iic n, X i of a dependent sequence of standard Borel spaces, except that the zeroth coordinate need only be measurable, is realized by a probability law on the whole sequence.

The result is stated directly in terms of prefix laws because this is the interface consumed by countable gluing constructions. Together with Mathlib's MeasureTheory.isProjectiveMeasureFamily_inducedFamily and MeasureTheory.isProjectiveLimit_nat_iff, it gives the usual Finset ℕ formulation.

theorem TauCeti.Measure.exists_isProjectiveLimit_nat {X : ℕ → Type u} [(n : ℕ) → MeasurableSpace (X n)] [∀ (n : ℕ), StandardBorelSpace (X (n + 1))] (P : (I : Finset ℕ) → MeasureTheory.Measure ((i : ↥I) → X ↑i)) [∀ (I : Finset ℕ), MeasureTheory.IsProbabilityMeasure (P I)] (hP : MeasureTheory.IsProjectiveMeasureFamily P) : ∃ (μ : MeasureTheory.Measure ((n : ℕ) → X n)), MeasureTheory.IsProbabilityMeasure μ ∧ MeasureTheory.IsProjectiveLimit μ P

Kolmogorov extension for a sequence with standard Borel positive coordinates. Every projective family of probability laws indexed by the finite subsets of ℕ has a projective limit, which is again a probability measure.

Mathlib already proves that this projective limit is unique; this theorem supplies existence by reducing to coherent prefixes and applying TauCeti.Measure.exists_map_frestrictLe_eq.