English
Let (X_i) be a family of measurable spaces indexed by ι. On the product space Ω = ∏_{i∈ι} X_i endowed with the product σ-algebra, for each finite set s ⊆ ι define F_s to be the σ-algebra consisting of sets that depend only on the coordinates in s (i.e., the σ-algebra generated by cylinder sets restricting to s). Then the family (F_s)_{s ∈ Finset ι} forms a filtration: if s ⊆ t, then F_s ⊆ F_t.
Русский
Пусть (X_i) — семейство измеримых пространств, индексируемое ι. На произведении Ω = ∏_{i∈ι} X_i с произведённой сигма-алгеброй задана система фильтраций F_s для каждого конечного подмножества s ⊆ ι: F_s состоит из множеств, зависящих только от координат в s (то есть порожденная цилиндрическими множителями на координаты из s). Тогда семейство (F_s) образует фильтрацию: если s ⊆ t, то F_s ⊆ F_t.
LaTeX
$$$\text{Let } (X_i)_{i\in\mathcal{I}} \text{ be a family of measurable spaces. Let } \Omega = \prod_{i\in\mathcal{I}} X_i \text{ with the product } \sigma ext{-algebra } \pi. \\ For each finite } S \subseteq \mathcal{I}, \\ \mathcal{F}_S := \sigma\Bigl(\{\{x \in \Omega : x|_S \in B\}\;:\; B \in \bigotimes_{i\in S} \mathcal{F}_i\}\Bigr). \\ Then the family (\mathcal{F}_S)_{S\in \mathrm{Finset}(\mathcal{I})} is a filtration, i.e. if $S \subseteq T$ then $\mathcal{F}_S \subseteq \mathcal{F}_T$.$$
Lean4
/-- The filtration of events which only depends on finitely many coordinates
on the product space `Π i, X i`, `piFinset s` consists of measurable sets depending only on
coordinates in `s`, where `s : Finset ι`. -/
def piFinset : @Filtration (Π i, X i) (Finset ι) _ pi
where
seq s := pi.comap s.restrict
mono' s t
hst := by
simp only
rw [← restrict₂_comp_restrict hst, ← comap_comp]
exact comap_mono (measurable_restrict₂ hst).comap_le
le' s := s.measurable_restrict.comap_le
