changeOriginSeries_summable_aux₂

English

A pure NN-real summability bound holds for sums of origin-changed terms, parameterized by r and k.

Русский

Пары ограничений суммируемости NN-real сохраняются для суммирования членов после переноса начала, зависящие от r и k.

LaTeX

$$$\\text{changeOriginSeries_summable_aux₃}: \\; \\forall r, k, \\dots$$$

Lean4

theorem changeOriginSeries_summable_aux₂ (hr : (r : ℝ≥0∞) < p.radius) (k : ℕ) :
    Summable fun s : Σ l : ℕ, { s : Finset (Fin (k + l)) // s.card = l } => ‖p (k + s.1)‖₊ * r ^ s.1 :=
  by
  rcases ENNReal.lt_iff_exists_add_pos_lt.1 hr with ⟨r', h0, hr'⟩
  simpa only [mul_inv_cancel_right₀ (pow_pos h0 _).ne'] using
    ((NNReal.summable_sigma.1 (p.changeOriginSeries_summable_aux₁ hr')).1 k).mul_right (r' ^ k)⁻¹

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