English
A measure ν is the projective limit of a family μ indexed by finite sets if and only if, for each n, ν restricted to the first n coordinates equals μ at Iic n. This reduces the verification to finite projections.
Русский
Мера ν является предельной по проекту семье μ, индексируемой по конечным множествам, если и только если для каждого n ограничение ν на первые n координат равно μ на Iic n. Это сводит проверку к конечным проекциям.
LaTeX
$$$ IsProjectiveLimit\nu\;μ\iff\forall n, \nu\map (frestrictLe\ n) = μ(Iic n) $$$
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`, where `n` is larger than
a given integer. -/
theorem isProjectiveLimit_nat_iff' {μ : (I : Finset ℕ) → Measure (Π i : I, X i)} (hμ : IsProjectiveMeasureFamily μ)
(ν : Measure (Π n, X n)) (a : ℕ) : IsProjectiveLimit ν μ ↔ ∀ ⦃n⦄, a ≤ n → ν.map (frestrictLe n) = μ (Iic n) :=
by
refine ⟨fun h n _ ↦ h (Iic n), fun h I ↦ ?_⟩
have := (I.subset_Iic_sup_id.trans (Iic_subset_Iic.2 (le_max_left (I.sup id) a)))
rw [← restrict₂_comp_restrict this, ← Measure.map_map, ← frestrictLe, h (le_max_right _ _), ← hμ]
all_goals fun_prop
