English
The canonical filtration on the product space Π i, X_i is given by piLE, with seq i = pi.comap (restrictLe i) and the structure is monotone in i.
Русский
Каноническая фильтрация на произведении Π_i X_i задаётся piLE по уровню i через сопряжение pi через ограничение частично упорядоченного индекса.
LaTeX
$$$\\text{piLE}(i)\\;\\text{has }\\text{seq }i=\\pi^{\\!\\!}\\!\\!_\\mathrm{comap}(\\mathrm{restrictLe}_i)$$$
Lean4
/-- The canonical filtration on the product space `Π i, X i`, where `piLE i`
consists of measurable sets depending only on coordinates `≤ i`. -/
def piLE : @Filtration (Π i, X i) ι _ pi
where
seq i := pi.comap (restrictLe i)
mono' i j
hij := by
simp only
rw [← restrictLe₂_comp_restrictLe hij, ← comap_comp]
exact comap_mono (measurable_restrictLe₂ _).comap_le
le' i := (measurable_restrictLe i).comap_le
