Half Binomial Coeff cauchy has Sum

import Mathlib.Algebra.BigOperators.NatAntidiagonal
import Mathlib.Analysis.Analytic.Binomial
import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.Normed.Ring.Basic
import Mathlib.Analysis.SpecificLimits.Normed
import Mathlib.Data.Sym.Basic
import Mathlib.Data.Sym.Card
import Mathlib.RingTheory.Binomial
import Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
import Definitions.Def_D1Bound5_HalfBinomialCoefficients_Definitions

section
namespace D1Bound5




theorem _root_.D1Bound5.halfBinomialCoeff_cauchy_hasSum (x y z : ℂ)
    (hx : ‖x * z‖ < 1) (hy : ‖y * z‖ < 1) :
    HasSum (fun n : ℕ => ∑ ij ∈ Finset.antidiagonal n,
      ((halfBinomialCoeff ij.1 : ℂ) * (x * z) ^ ij.1) *
      ((halfBinomialCoeff ij.2 : ℂ) * (y * z) ^ ij.2))
      (((1 + x * z) ^ (1 / 2 : ℂ)) * ((1 + y * z) ^ (1 / 2 : ℂ))) := by sorry





end D1Bound5
end