summable_norm_apply — Mathlib

English

There is a summability result for the nnnorm of p_n applied to x within radius_ball.

Русский

Суммируемость сохраняется для nnnorm коэффициентов p_n при применении к x внутри радиуса.

LaTeX

$$$x \\in \\mathrm{EMetric.ball}(0, p.radius) \\Rightarrow \\sum_{n} \\|p_n(x)\\|_{} < \\infty.$$$

Lean4

theorem summable_norm_apply (p : FormalMultilinearSeries 𝕜 E F) {x : E} (hx : x ∈ EMetric.ball (0 : E) p.radius) :
    Summable fun n : ℕ => ‖p n fun _ => x‖ :=
  by
  rw [mem_emetric_ball_zero_iff] at hx
  refine .of_nonneg_of_le (fun _ ↦ norm_nonneg _) (fun n ↦ ((p n).le_opNorm _).trans_eq ?_) (p.summable_norm_mul_pow hx)
  simp

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