English
From a projective family of measures μ on coordinate spaces, one defines a family indexed by finite sets S by pushing forward μ via the restriction to S. This provides a finite-dimensional marginal system consistent with μ.
Русский
Из проективной семьи мер μ на пространства координат определяется семейство, индексируемое конечными множествами S, получаемое через сдвиг меры μ ограниченно до S. Это обеспечивает согласованную конечномерную маргинальную систему.
LaTeX
$$$ inducedFamily\;μ\;S = (μ(S^{\mathrm{sup} id})).map(restrict₂ S.subset_Iic_sup_id) $$$
Lean4
/-- To check that a measure `ν` is the projective limit of a projective family of measures indexed
by `Finset ℕ`, it is enough to check on intervals of the form `Iic n`. -/
theorem isProjectiveLimit_nat_iff {μ : (I : Finset ℕ) → Measure (Π i : I, X i)} (hμ : IsProjectiveMeasureFamily μ)
(ν : Measure (Π n, X n)) : IsProjectiveLimit ν μ ↔ ∀ n, ν.map (frestrictLe n) = μ (Iic n) :=
by
rw [isProjectiveLimit_nat_iff' hμ _ 0]
simp
