tendstoInMeasure_of_tendsto_eLpNorm

English

Convergence in Lp implies convergence in measure, capturing a generalization over Lp spaces.

Русский

Сходимость в Lp подразумевает сходимость по мере, обобщая на пространства Lp.

LaTeX

$$$p \in \mathbb{R}_{>0} \Rightarrow TendstoInMeasure μ f l g \Leftarrow Tendsto (n \mapsto eLpNorm (f n - g) p μ) l (nhds 0)$$$

Lean4

/-- Convergence in Lp implies convergence in measure. -/
theorem tendstoInMeasure_of_tendsto_eLpNorm {l : Filter ι} (hp_ne_zero : p ≠ 0) (hf : ∀ n, AEStronglyMeasurable (f n) μ)
    (hg : AEStronglyMeasurable g μ) (hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) l (𝓝 0)) :
    TendstoInMeasure μ f l g := by
  by_cases hp_ne_top : p = ∞
  · subst hp_ne_top
    exact tendstoInMeasure_of_tendsto_eLpNorm_top hfg
  · exact tendstoInMeasure_of_tendsto_eLpNorm_of_ne_top hp_ne_zero hp_ne_top hf hg hfg

Похожие утверждения