Documentation

LeanPool.CarlsonFunctions.Pochhammer.Gamma

Pochhammer identities for the Gamma function #

This file is a temporary home for identities connecting Mathlib's Gamma function and ascending Pochhammer polynomials. The reciprocal formulation remains valid at the poles of Gamma.

source
theorem Complex.one_div_Gamma_eq_ascPochhammer_mul_one_div_Gamma_add_nat (z : ℂ) (n : ℕ) :
(Gamma z)⁻¹ = Polynomial.eval z (ascPochhammer ℂ n) * (Gamma (z + ↑n))⁻¹

The natural-shift recurrence for reciprocal Gamma, valid at every complex argument. This is the pole-free counterpart of expressing an ascending Pochhammer symbol as a quotient of Gamma functions.

source
theorem Complex.inv_Gamma_add_nat_of_ne_zero {s : ℂ} {n : ℕ} (h : ∀ k < n, s + ↑k ≠ 0) :
(Gamma (s + ↑n))⁻¹ = (Gamma s)⁻¹ * ∏ k ∈ Finset.range n, (s + ↑k)⁻¹

Reciprocal Gamma after a natural shift, as a product of reciprocals, provided none of the intermediate points is a non-positive integer.

source
theorem Complex.ascPochhammer_eval_split_reflection (c : ℂ) {m n : ℕ} (hmn : m ≤ n) :
Polynomial.eval c (ascPochhammer ℂ n) = (-1) ^ (n - m) * Polynomial.eval c (ascPochhammer ℂ m) * Polynomial.eval (1 - c - ↑n) (ascPochhammer ℂ (n - m))

Splitting an ascending Pochhammer symbol and reflecting the remaining factors.

The multiplicative form remains valid when one of the Pochhammer factors vanishes, unlike the corresponding quotient identity.

source
theorem Real.gamma_add_nat_div_gamma_eq_ascPochhammer (x : ℝ) (hx : 0 < x) (n : ℕ) :
Gamma (x + ↑n) / Gamma x = Polynomial.eval x (ascPochhammer ℝ n)

A quotient of gamma values separated by a natural number equals the corresponding rising factorial.

Gamma regularity and decay under natural shifts #

The historical DirichletTransform names are retained; these results are scalar and independent of simplex measures or Carlson functions.

source
def DirichletTransform.IsCarlsonGammaRegular (w : ℂ) :
Prop

Carlson's set U: complex numbers that are not nonpositive integers, equivalently the finite points at which the Gamma function has no pole.

Equations
Instances For
    source
    theorem DirichletTransform.IsCarlsonGammaRegular.add_nat {w : ℂ} (hw : IsCarlsonGammaRegular w) (m : ℕ) :
    IsCarlsonGammaRegular (w + ↑m)

    Positive integral shifts preserve Gamma regularity.

    source
    theorem DirichletTransform.IsCarlsonGammaRegular.ascPochhammer_ne_zero {w : ℂ} (hw : IsCarlsonGammaRegular w) (n : ℕ) :
    Polynomial.eval w (ascPochhammer ℂ n) ≠ 0

    No ascending Pochhammer factor vanishes at a Gamma-regular argument.

    source
    theorem DirichletTransform.norm_invGamma_add_nat_le {s : ℂ} (hs : 1 ≤ s.re) (n : ℕ) :
    ‖(Complex.Gamma (s + ↑n))⁻¹‖ ≤ ‖(Complex.Gamma s)⁻¹‖ / ↑n.factorial

    Reciprocal Gamma gains at least factorial decay under positive integer shifts in the half-plane 1 ≤ re s.