Bennett negative half abs

Proved

D1Bound5.bennett_negative_half_abs

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

diophantine-tuplesnumber-theory

The absolute negative-half tail is the same positive ascending product.

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_negative_half_abs (m : ℕ) :
    (m.factorial : ℝ) * |Ring.choose (-1 / 2 : ℝ) m| =
      (ascPochhammer ℝ m).eval (1 / 2) := by sorry





end D1Bound5
end

Source

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

View graph