English
The limitProcess f ℱ μ is strongly measurable with respect to m.
Русский
LimitProcess f ℱ μ является сильно измеримой относительно m.
LaTeX
$$$\\text{StronglyMeasurable}_{m}(\\mathrm{limitProcess}\\, f\\, \\mathcal F\\, \\mu)$$$
Lean4
/-- Given a process `f` and a filtration `ℱ`, if `f` converges to some `g` almost everywhere and
`g` is `⨆ n, ℱ n`-measurable, then `limitProcess f ℱ μ` chooses said `g`, else it returns 0.
This definition is used to phrase the a.e. martingale convergence theorem
`Submartingale.ae_tendsto_limitProcess` where an L¹-bounded submartingale `f` adapted to `ℱ`
converges to `limitProcess f ℱ μ` `μ`-almost everywhere. -/
noncomputable def limitProcess (f : ι → Ω → E) (ℱ : Filtration ι m) (μ : Measure Ω) :=
if h : ∃ g : Ω → E, StronglyMeasurable[⨆ n, ℱ n] g ∧ ∀ᵐ ω ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω)) then
Classical.choose h
else 0
