Bennett Cleared Taylor eval

import Lean.Elab.Tactic.Omega
import Mathlib.Algebra.Polynomial.BigOperators
import Mathlib.Algebra.Polynomial.Degree.Operations
import Mathlib.RingTheory.PowerSeries.Binomial
import Mathlib.Tactic.Ring
import Definitions.Def_D1Bound5_BennettClearedResidues_Definitions

section
open Finset

namespace D1Bound5

variable {F : Type*} [Field F] [CharZero F]






theorem _root_.D1Bound5.bennettClearedTaylor_eval (k r : ℕ) (hr : r ≤ k) (ν a N : F)
    (B : PowerSeries F) (hd : N + a ≠ 0) :
    (bennettClearedTaylor k r ν a B).eval N =
      (N + a) ^ k * PowerSeries.coeff r
        (PowerSeries.rescale (N + a)⁻¹
          (PowerSeries.binomialSeries F ((k : F) + ν)) * B) := by sorry



section Nodes

variable {I : Type*} [DecidableEq I]

















end Nodes

end D1Bound5
end