Bennett coeff mul norm le

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

section
open Finset

namespace D1Bound5






theorem _root_.D1Bound5.bennett_coeff_mul_norm_le
    (B C : PowerSeries ℂ) (D E : PowerSeries ℝ)
    (hB : ∀ h, ‖PowerSeries.coeff h B‖ ≤ PowerSeries.coeff h D)
    (hC : ∀ h, ‖PowerSeries.coeff h C‖ ≤ PowerSeries.coeff h E) (t : ℕ) :
    ‖PowerSeries.coeff t (B * C)‖ ≤ PowerSeries.coeff t (D * E) := by sorry











end D1Bound5
end