Bennett rescaled binomial has Sum

import Lean.Elab.Tactic.Omega
import Mathlib.Algebra.Polynomial.BigOperators
import Mathlib.Algebra.Polynomial.Degree.Operations
import Mathlib.Algebra.Polynomial.Div
import Mathlib.Algebra.Polynomial.PartialFractions
import Mathlib.Algebra.Polynomial.RingDivision
import Mathlib.Analysis.Analytic.Binomial
import Mathlib.Analysis.Normed.Ring.InfiniteSum
import Mathlib.LinearAlgebra.Matrix.Polynomial
import Mathlib.RingTheory.PowerSeries.Binomial
import Mathlib.RingTheory.PowerSeries.Trunc
import Mathlib.Tactic.Ring

section
open Finset

namespace D1Bound5




theorem _root_.D1Bound5.bennett_rescaled_binomial_hasSum (a ν x : ℂ) (hx : ‖a * x‖ < 1) :
    HasSum (fun r : ℕ =>
      PowerSeries.coeff r (PowerSeries.rescale a (PowerSeries.binomialSeries ℂ ν)) *
        x ^ r) ((1 + a * x) ^ ν) ∧
    Summable (fun r : ℕ =>
      ‖PowerSeries.coeff r
        (PowerSeries.rescale a (PowerSeries.binomialSeries ℂ ν)) * x ^ r‖) := by sorry

section Nodes

variable {I : Type*} [Fintype I] [DecidableEq I]







end Nodes

end D1Bound5
end