English
If μ is projective in the sense that projecting from μ_b to μ_a along hab ≤ b preserves the measure (i.e., (μ_b).map (frestrictLe₂ hab) = μ_a for a ≤ b), then the inducedFamily μ is a projective measure family.
Русский
Если μ является проективным семейством в смысле сохранения меры под проекциями, то индуцированное семейство μ также является проективным семейством мер.
LaTeX
$$$\\bigl(\\forall a,b:\\mathbb{N},\\; a\\le b,\\ (μ_b).map(\\frestrictLe₂\\ hab)=μ_a\\bigr) \\Rightarrow \\text{IsProjectiveMeasureFamily} (inducedFamily μ)$$$
Lean4
/-- Given a family of measures `μ : (n : ℕ) → Measure (Π i : Iic n, X i)`, the induced family
will be projective only if `μ` is projective, in the sense that if `a ≤ b`, then projecting
`μ b` gives `μ a`. -/
theorem isProjectiveMeasureFamily_inducedFamily (h : ∀ a b : ℕ, ∀ hab : a ≤ b, (μ b).map (frestrictLe₂ hab) = μ a) :
IsProjectiveMeasureFamily (inducedFamily μ) := by
intro I J hJI
have sls : J.sup id ≤ I.sup id := sup_mono hJI
simp only [inducedFamily]
rw [Measure.map_map, restrict₂_comp_restrict₂, ← restrict₂_comp_restrict₂ J.subset_Iic_sup_id (Iic_subset_Iic.2 sls),
← Measure.map_map, ← frestrictLe₂.eq_def sls, h (J.sup id) (I.sup id) sls]
all_goals fun_prop
