tendstoInMeasure_of_tendsto_Lp — Mathlib

English

Convergence in Lp implies convergence in measure for general Lp with p ≠ 0.

Русский

Сходимость в Lp означает сходимость по мере для общего p ≠ 0.

LaTeX

$$$p \ne 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_Lp [hp : Fact (1 ≤ p)] {f : ι → Lp E p μ} {g : Lp E p μ} {l : Filter ι}
    (hfg : Tendsto f l (𝓝 g)) : TendstoInMeasure μ (fun n => f n) l g :=
  tendstoInMeasure_of_tendsto_eLpNorm (zero_lt_one.trans_le hp.elim).ne.symm (fun _ => Lp.aestronglyMeasurable _)
    (Lp.aestronglyMeasurable _) ((Lp.tendsto_Lp_iff_tendsto_eLpNorm' _ _).mp hfg)

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