Bennett factorial mul abs choose

Proved

D1Bound5.bennett_factorial_mul_abs_choose

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

diophantine-tuplesnumber-theory

Absolute generalized choose coefficients retain the ordinary factorial denominator and the actual descending Pochhammer numerator.

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_factorial_mul_abs_choose (r : ℝ) (n : ℕ) :
    (n.factorial : ℝ) * |Ring.choose r n| = |(descPochhammer ℝ n).eval r| := by sorry









end D1Bound5
end

Source

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

View graph