Bennett two residual choose abs Gamma

import Lean.Elab.Tactic.Omega
import Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
import Mathlib.RingTheory.Binomial
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.LinearCombination
import Mathlib.Tactic.Positivity

section
open Polynomial

namespace D1Bound5














theorem _root_.D1Bound5.bennett_two_residual_choose_abs_Gamma (k : ℕ) (hk : 1 ≤ k) :
    |Ring.choose ((k : ℝ) + 1 / 2) (3 * k)| =
      Real.Gamma ((k : ℝ) + 3 / 2) * Real.Gamma (2 * (k : ℝ) - 1 / 2) /
        (Real.pi * Real.Gamma (3 * (k : ℝ) + 1)) := by sorry

end D1Bound5
end