English
Under IsFiniteMeasure μ, Submartingale f with bounded filtration has a trimmed almost-everywhere limit: there exists g such that Tendsto of f_n on a filtered set to a limit exists.
Русский
При мера μ конечна и субмартингал f с ограниченной фильтрацией имеет усечённое почти всюду предел: существует g, к которому сходятся f_n на подходящем множестве.
LaTeX
$$$\\exists g,\\ Tendsto(f_n(\\omega))_{n\\to\\infty} = c \\,\\text{a.e.}$ на тримированной мере.$$
Lean4
theorem exists_ae_trim_tendsto_of_bdd [IsFiniteMeasure μ] (hf : Submartingale f ℱ μ)
(hbdd : ∀ n, eLpNorm (f n) 1 μ ≤ R) :
∀ᵐ ω ∂μ.trim (sSup_le fun _ ⟨_, hn⟩ => hn ▸ ℱ.le _ : ⨆ n, ℱ n ≤ m0), ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c) :=
by
letI := (⨆ n, ℱ n)
rw [ae_iff, trim_measurableSet_eq]
· exact hf.exists_ae_tendsto_of_bdd hbdd
·
exact
MeasurableSet.compl <|
measurableSet_exists_tendsto fun n => (hf.stronglyMeasurable n).measurable.mono (le_sSup ⟨n, rfl⟩) le_rfl
