hasSum_norm — Mathlib

English

The sequence ‖f i‖^{p.toReal} has sum ‖f‖^{p.toReal}. In particular, HasSum(‖f i‖^{p.toReal}) with sum ‖f‖^{p.toReal}.

Русский

Последовательность коэффициентов ‖f_i‖^{p.toReal} сходится, сумма равна ‖f‖^{p.toReal}.

LaTeX

$$$$ \operatorname{HasSum}\left( i \mapsto \|f_i\|^{p^{\mathrm{toReal}}}, \|f\|^{p^{\mathrm{toReal}}} \right). $$$$

Lean4

theorem hasSum_norm (hp : 0 < p.toReal) (f : lp E p) : HasSum (fun i => ‖f i‖ ^ p.toReal) (‖f‖ ^ p.toReal) :=
  by
  rw [norm_rpow_eq_tsum hp]
  exact ((lp.memℓp f).summable hp).hasSum

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