cauchySeq_Lp_iff_cauchySeq_eLpNorm

English

Cauchy sequences in Lp correspond to Cauchy sequences of eLpNorm in the ambient space.

Русский

Циклы Лп соответствуют Циклам тяжёлого пространства через eLpNorm.

LaTeX

$$$CauchySeq(f) \leftrightarrow Tendsto( (f_n - f_m), atTop, 0)$$$

Lean4

theorem cauchySeq_Lp_iff_cauchySeq_eLpNorm {ι} [Nonempty ι] [SemilatticeSup ι] [hp : Fact (1 ≤ p)] (f : ι → Lp E p μ) :
    CauchySeq f ↔ Tendsto (fun n : ι × ι => eLpNorm (⇑(f n.fst) - ⇑(f n.snd)) p μ) atTop (𝓝 0) :=
  by
  simp_rw [cauchySeq_iff_tendsto_dist_atTop_0, dist_def]
  rw [← ENNReal.toReal_zero, ENNReal.tendsto_toReal_iff (fun n => ?_) ENNReal.zero_ne_top]
  rw [eLpNorm_congr_ae (Lp.coeFn_sub _ _).symm]
  exact eLpNorm_ne_top _

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