changeOriginSeries_summable_aux₃

English

A uniform summability bound across origin-changed terms is given by the radius and a power bound.

Русский

Суммируемость единообразная по всем измененным началам дает границу, зависящую от радиуса и степенного предела.

LaTeX

$$$\\text{changeOriginSeries_summable_aux₄}: \\; (radius) \\Rightarrow \\; \\text{Summable } \\dots$$$

Lean4

theorem changeOriginSeries_summable_aux₃ {r : ℝ≥0} (hr : ↑r < p.radius) (k : ℕ) :
    Summable fun l : ℕ => ‖p.changeOriginSeries k l‖₊ * r ^ l :=
  by
  refine NNReal.summable_of_le (fun n => ?_) (NNReal.summable_sigma.1 <| p.changeOriginSeries_summable_aux₂ hr k).2
  simp only [NNReal.tsum_mul_right]
  gcongr
  apply p.nnnorm_changeOriginSeries_le_tsum

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