English
Under suitable hypotheses (e.g., β with a multiplicative structure and indicator functions), filtrationOfSet hsm equals Filtration.natural generated by indicator functions of s_i.
Русский
При подходящих условиях filtrationOfSet hsm равна Filtration.natural, порождённой индикаторными функциями множеств s_i.
LaTeX
$$$\\mathrm{filtrationOfSet}(hsm) = \\mathrm{Filtration.natural}(i \\mapsto (s_i).indicator(1))$$$
Lean4
/-- Given a sequence of functions, the natural filtration is the smallest sequence
of σ-algebras such that the sequence of functions is measurable with respect to
the filtration. -/
def natural (u : ι → Ω → β) (hum : ∀ i, StronglyMeasurable (u i)) : Filtration ι m
where
seq i := ⨆ j ≤ i, MeasurableSpace.comap (u j) mβ
mono' _ _ hij := biSup_mono fun _ => ge_trans hij
le'
i := by
refine iSup₂_le ?_
rintro j _ s ⟨t, ht, rfl⟩
exact (hum j).measurable ht
