Bennett Gamma half add nat

Proved

D1Bound5.bennett_Gamma_half_add_nat

by tp · Oct 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

diophantine-tuplesnumber-theory

Positive half-integer Gamma values expressed by the actual ascending Pochhammer polynomial. Only Gamma's proved recurrence is used.

Preamble

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

Formal statement

section
open Polynomial

namespace D1Bound5


theorem _root_.D1Bound5.bennett_Gamma_half_add_nat (n : ℕ) :
    Real.Gamma ((1 / 2 : ℝ) + n) =
      Real.Gamma (1 / 2 : ℝ) * (ascPochhammer ℝ n).eval (1 / 2) := by sorry













end D1Bound5
end

Source

D1Bound5/BennettChooseGamma.lean, lines 12-27, SHA-256 ed364c7393e2791f97fcc92aa240c1e9f11c109de4d2306c76becc3f16ded4f0. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph