English
For a finite measure μ and a submartingale f with bounded L¹-norm, there exists a limit process ℱ.limitProcess(f, μ) to which f_n converges almost everywhere (along a subsequence if needed).
Русский
Для конечной меры μ и субмартингала f с ограниченной L¹-нормой существует предел процесс ∂ℱ.limitProcess(f, μ), к которому f_n сходится почти surely.
LaTeX
$$$\\forall^{\\mathrm{a.e.}} \\omega,\\; f_n(\\omega) \\to \\text{limitProcess}(f,\\mathcal{F},\\mu,ω).$$$
Lean4
/-- **Almost everywhere martingale convergence theorem**: An L¹-bounded submartingale converges
almost everywhere to a `⨆ n, ℱ n`-measurable function. -/
theorem ae_tendsto_limitProcess [IsFiniteMeasure μ] (hf : Submartingale f ℱ μ) (hbdd : ∀ n, eLpNorm (f n) 1 μ ≤ R) :
∀ᵐ ω ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (ℱ.limitProcess f μ ω)) := by
classical
suffices ∃ g, StronglyMeasurable[⨆ n, ℱ n] g ∧ ∀ᵐ ω ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω))
by
rw [limitProcess, dif_pos this]
exact (Classical.choose_spec this).2
set g' : Ω → ℝ := fun ω => if h : ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c) then h.choose else 0
have hle : ⨆ n, ℱ n ≤ m0 := sSup_le fun m ⟨n, hn⟩ => hn ▸ ℱ.le _
have hg' : ∀ᵐ ω ∂μ.trim hle, Tendsto (fun n => f n ω) atTop (𝓝 (g' ω)) :=
by
filter_upwards [hf.exists_ae_trim_tendsto_of_bdd hbdd] with ω hω
simp_rw [g', dif_pos hω]
exact hω.choose_spec
have hg'm : AEStronglyMeasurable[⨆ n, ℱ n] g' (μ.trim hle) :=
(@aemeasurable_of_tendsto_metrizable_ae' _ _ (⨆ n, ℱ n) _ _ _ _ _ _ _
(fun n => ((hf.stronglyMeasurable n).measurable.mono (le_sSup ⟨n, rfl⟩ : ℱ n ≤ ⨆ n, ℱ n) le_rfl).aemeasurable)
hg').aestronglyMeasurable
obtain ⟨g, hgm, hae⟩ := hg'm
have hg : ∀ᵐ ω ∂μ.trim hle, Tendsto (fun n => f n ω) atTop (𝓝 (g ω)) :=
by
filter_upwards [hae, hg'] with ω hω hg'ω
exact hω ▸ hg'ω
exact ⟨g, hgm, measure_eq_zero_of_trim_eq_zero hle hg⟩
