Bennett Numerator Majorant has Sum

import Lean.Elab.Tactic.Omega
import Mathlib.Algebra.Polynomial.BigOperators
import Mathlib.Algebra.Polynomial.Degree.Operations
import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.Normed.Ring.InfiniteSum
import Mathlib.RingTheory.PowerSeries.Binomial
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Positivity
import Mathlib.Tactic.Ring
import Definitions.Def_D1Bound5_BennettCoefficientMajorant_Definitions

section
open Finset

namespace D1Bound5














theorem _root_.D1Bound5.bennettNumeratorMajorant_hasSum (U r : ℝ) (k : ℕ) :
    HasSum (fun h : ℕ => PowerSeries.coeff h (bennettNumeratorMajorant U k) * r ^ h)
      ((U + r) ^ (k + 1) / U) := by sorry



end D1Bound5
end