3.1. Gamma-function identities🔗

Lemma3.1.1

uses 0

Used by 3

Reverse dependency previews

Preview

Lemma 3.1.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

For all complex z away from the poles, \Gamma(z+1) = z\Gamma(z) and \Gamma(z)\Gamma(1-z) = \pi/\sin(\pi z); moreover \Gamma(\bar z) = \overline{\Gamma(z)}.

Lean code for Lemma3.1.1●3 theorems

theoremdefined in Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean

complete

theorem Complex.Gamma_add_one (s : ℂ) (h2 : s ≠ 0) :
  Complex.Gamma (s + 1) = s * Complex.Gamma s

theorem Complex.Gamma_add_one (s : ℂ)
  (h2 : s ≠ 0) :
  Complex.Gamma (s + 1) =
    s * Complex.Gamma s

The recurrence relation for the `Γ` function.

theoremdefined in Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean

complete

theorem Complex.Gamma_mul_Gamma_one_sub (z : ℂ) :
  Complex.Gamma z * Complex.Gamma (1 - z) =
    ↑Real.pi / Complex.sin (↑Real.pi * z)

theorem Complex.Gamma_mul_Gamma_one_sub (z : ℂ) :
  Complex.Gamma z *
      Complex.Gamma (1 - z) =
    ↑Real.pi / Complex.sin (↑Real.pi * z)

Euler's reflection formula for the complex Gamma function.

theoremdefined in Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean

complete

theorem Complex.Gamma_conj (s : ℂ) :
  Complex.Gamma ((starRingEnd ℂ) s) = (starRingEnd ℂ) (Complex.Gamma s)

theorem Complex.Gamma_conj (s : ℂ) :
  Complex.Gamma ((starRingEnd ℂ) s) =
    (starRingEnd ℂ) (Complex.Gamma s)

Proof for Lemma 3.1.1

uses 0

The recurrence, reflection and conjugation formulas are standard (Mathlib).

Lemma3.1.2

uses 1used by 1✓L∃∀N

Iterating the recurrence of Lemma 3.1.1, \Gamma(z+k) = \Gamma(z)\prod_{j<k}(z+j) for k \in \mathbb{N} and z \notin -\mathbb{N}.

Lean code for Lemma3.1.2●1 theorem

theoremdefined in CohnElkiesForMathlib/Analysis/SpecialFunctions/Gamma/Basic.lean

complete

theorem Complex.Gamma_add_nat_eq_mul_prod (z : ℂ) (hz : ∀ (j : ℕ), z + ↑j ≠ 0)
  (k : ℕ) :
  Complex.Gamma (z + ↑k) =
    Complex.Gamma z * ∏ j ∈ Finset.range k, (z + ↑j)

theorem Complex.Gamma_add_nat_eq_mul_prod (z : ℂ)
  (hz : ∀ (j : ℕ), z + ↑j ≠ 0) (k : ℕ) :
  Complex.Gamma (z + ↑k) =
    Complex.Gamma z *
      ∏ j ∈ Finset.range k, (z + ↑j)

The gamma recurrence `Γ(z + k) = Γ(z) ∏_{j < k} (z + j)`.

Proof for Lemma 3.1.2

uses 0

Induction on k.

Lemma3.1.3

uses 0

Used by 8

Reverse dependency previews

Preview

Lemma 4.1.25

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

For real b \ne 0 (equation (7)), |\Gamma(ib)|^2 = \dfrac{\pi}{b\sinh(\pi b)}, |\Gamma(1/2 + ib)|^2 = \dfrac{\pi}{\cosh(\pi b)}, and |\Gamma(-ib)| = |\Gamma(ib)|.

Lean code for Lemma3.1.3●2 theorems

theoremdefined in CohnElkiesForMathlib/Analysis/SpecialFunctions/Gamma/Beta.lean

complete

theorem Complex.norm_Gamma_I_mul_sq {x : ℝ} (hx : x ≠ 0) :
  ‖Complex.Gamma (Complex.I * ↑x)‖ ^ 2 =
    Real.pi / (x * Real.sinh (Real.pi * x))

theorem Complex.norm_Gamma_I_mul_sq {x : ℝ}
  (hx : x ≠ 0) :
  ‖Complex.Gamma (Complex.I * ↑x)‖ ^ 2 =
    Real.pi /
      (x * Real.sinh (Real.pi * x))

`|Γ(ib)|² = π / (b sinh(πb))`; report (7).

theoremdefined in CohnElkiesForMathlib/Analysis/SpecialFunctions/Gamma/Beta.lean

complete

theorem Complex.norm_Gamma_one_half_add_I_mul_sq (x : ℝ) :
  ‖Complex.Gamma (1 / 2 + Complex.I * ↑x)‖ ^ 2 =
    Real.pi / Real.cosh (Real.pi * x)

theorem Complex.norm_Gamma_one_half_add_I_mul_sq
  (x : ℝ) :
  ‖Complex.Gamma
          (1 / 2 + Complex.I * ↑x)‖ ^
      2 =
    Real.pi / Real.cosh (Real.pi * x)

`|Γ(1/2 + ib)|² = π / cosh(πb)`; report (7).

Proof for Lemma 3.1.3

uses 1

Definition3.1.4

uses 0

Used by 7

Reverse dependency previews

Preview

Lemma 3.1.5

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

The digamma function is \psi = \Gamma'/\Gamma, the logarithmic derivative of \Gamma; on the positive real axis, \psi = (\log\Gamma)'. Its derivatives are the trigamma function \psi' and \psi''. (In Lean, the real digamma function is the real part of Mathlib's Complex.digamma, which equals the logarithmic derivative of Real.Gamma, Real.digamma_eq_logDeriv_Gamma.)

Lean code for Definition3.1.4●1 definition

defdefined in CohnElkiesForMathlib/Analysis/SpecialFunctions/Gamma/Digamma.lean

complete

def Real.digamma (x : ℝ) : ℝ

def Real.digamma (x : ℝ) : ℝ

The real digamma function `ψ = Γ'/Γ`, the real part of `Complex.digamma`.

Lemma3.1.5

uses 1used by 1✓L∃∀N

With \psi as in Definition 3.1.4, \log(x-1) \le \psi(x) \le \log x for real x > 1.

Lean code for Lemma3.1.5●1 theorem

theoremdefined in CohnElkiesForMathlib/Analysis/SpecialFunctions/Gamma/Digamma.lean

complete

theorem Real.log_sub_one_le_digamma_le_log {x : ℝ} (hx : 1 < x) :
  Real.log (x - 1) ≤ x.digamma ∧ x.digamma ≤ Real.log x

theorem Real.log_sub_one_le_digamma_le_log {x : ℝ}
  (hx : 1 < x) :
  Real.log (x - 1) ≤ x.digamma ∧
    x.digamma ≤ Real.log x

`log (x - 1) ≤ ψ(x) ≤ log x` for `x > 1`, from the convexity of `log Γ`.

Proof for Lemma 3.1.5

uses 0

\log\Gamma is convex on (0,\infty) with \log\Gamma(x+1) - \log\Gamma(x) = \log x, so its derivative \psi satisfies \log(x-1) = \log\Gamma(x) - \log\Gamma(x-1) \le \psi(x) \le \log\Gamma(x+1) - \log\Gamma(x) = \log x for x > 1.

Lemma3.1.6

uses 1

Used by 3

Reverse dependency previews

Preview

Lemma 3.1.7

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

With \psi as in Definition 3.1.4, \psi(x) - \log x \to 0 as real x \to +\infty.

Lean code for Lemma3.1.6●1 theorem

theoremdefined in CohnElkiesForMathlib/Analysis/SpecialFunctions/Gamma/Digamma.lean

complete

theorem Real.tendsto_digamma_sub_log_atTop :
  Filter.Tendsto (fun x ↦ x.digamma - Real.log x) Filter.atTop (nhds 0)

theorem Real.tendsto_digamma_sub_log_atTop :
  Filter.Tendsto
    (fun x ↦ x.digamma - Real.log x)
    Filter.atTop (nhds 0)

`ψ(x) - log x → 0` as `x → ∞`.

Proof for Lemma 3.1.6

uses 1

By Lemma 3.1.5, \log(x-1) - \log x \le \psi(x) - \log x \le 0, and \log x - \log(x-1) \to 0. (The report uses the sharper Stirling expansion \psi(x) = \log x - 1/(2x) + O(x^{-2}), together with trigamma and polygamma bounds and the Binet-type representation of \log\Gamma; the formalization replaces these by explicit moment bounds for the gamma damping density, Lemma 5.3.12, by the Binet-type representation Lemma 5.3.5, and by polynomial decay of \Gamma along vertical lines.)

Lemma3.1.7

uses 1used by 1✓L∃∀N

(Gauss's integral.) For real m > 0, with \psi as in Definition 3.1.4, \psi(m) = \int_0^\infty\Bigl(\dfrac{e^{-t}}{t} - \dfrac{e^{-mt}}{1 - e^{-t}}\Bigr)\,dt, the integrand being integrable on (0,\infty).

Lean code for Lemma3.1.7●1 theorem

theoremdefined in CohnElkiesForMathlib/Analysis/SpecialFunctions/Gamma/DigammaIntegral.lean

complete

theorem Real.digamma_eq_integral {m : ℝ} (hm : 0 < m) :
  m.digamma =
    ∫ (t : ℝ) in Set.Ioi 0,
      Real.exp (-t) / t - Real.exp (-m * t) / (1 - Real.exp (-t))

theorem Real.digamma_eq_integral {m : ℝ}
  (hm : 0 < m) :
  m.digamma =
    ∫ (t : ℝ) in Set.Ioi 0,
      Real.exp (-t) / t -
        Real.exp (-m * t) /
          (1 - Real.exp (-t))

Gauss's integral representation of the digamma function.

Proof for Lemma 3.1.7

uses 1

By the recurrence \psi(m+1) = \psi(m) + 1/m and \psi(x) - \log x \to 0 (Lemma 3.1.6), \psi(m) = \lim_n\bigl(\log n - \sum_{k=0}^n (m+k)^{-1}\bigr). For n \ge 1, Frullani's formula \log n = \int_0^\infty (e^{-t} - e^{-nt})/t\,dt and (m+k)^{-1} = \int_0^\infty e^{-(m+k)t}\,dt with the geometric sum \sum_{k=0}^n e^{-(m+k)t} = e^{-mt}(1 - e^{-(n+1)t})/(1 - e^{-t}) write the n-th term as \int_0^\infty\bigl[(e^{-t}/t - e^{-mt}/(1-e^{-t})) - e^{-nt}g(t)\bigr]dt with g(t) = 1/t - e^{-(m+1)t}/(1-e^{-t}). Since 0 \le g \le m + 1 on (0,\infty), the correction is at most (m+1)/n in absolute value and tends to 0.

Lemma3.1.8

uses 1

Used by 5

Reverse dependency previews

Preview

Theorem 1.1.10

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

With v_d from Definition 1.1.3, \log v_d/d + \log d/2 \to (\log(2\pi) + 1)/2 as d \to \infty; equivalently v_d^{1/d}\sqrt d \to \sqrt{2\pi e}, i.e. v_d^{1/d} = (1+o(1))\sqrt{2\pi e/d}, and (v_d/2^d)^{1/d}\sqrt d \to \sqrt{2\pi e}/2.

Lean code for Lemma3.1.8●2 theorems

theoremdefined in CohnElkies/Asymptotics/Stirling.lean

complete

theorem CohnElkies.tendsto_normalizedVolumeLog :
  Filter.Tendsto CohnElkies.normalizedVolumeLog Filter.atTop
    (nhds ((Real.log (2 * Real.pi) + 1) / 2))

theorem CohnElkies.tendsto_normalizedVolumeLog :
  Filter.Tendsto
    CohnElkies.normalizedVolumeLog
    Filter.atTop
    (nhds
      ((Real.log (2 * Real.pi) + 1) / 2))

theoremdefined in CohnElkies/Asymptotics/Stirling.lean

complete

theorem CohnElkies.tendsto_packingGeometricRoot :
  Filter.Tendsto CohnElkies.packingGeometricRoot Filter.atTop
    (nhds (√(2 * Real.pi * Real.exp 1) / 2))

theorem CohnElkies.tendsto_packingGeometricRoot :
  Filter.Tendsto
    CohnElkies.packingGeometricRoot
    Filter.atTop
    (nhds
      (√(2 * Real.pi * Real.exp 1) / 2))

Stirling's formula for the geometric factor: `(v_d/2^d)^{1/d} √d → √(2πe)/2` (report (28)).

Proof for Lemma 3.1.8

uses 0

By Stirling's formula, \log\Gamma(d/2+1) = (d/2)\log(d/2) - d/2 + O(\log d), so \tfrac1d\log v_d = \tfrac12\log\pi - \tfrac12\log(d/2) + \tfrac12 + O(\tfrac{\log d}{d}), which is \tfrac12\log\tfrac{2\pi e}{d} + o(1). Since Mathlib has Stirling's formula for factorials but not for \Gamma on the half-integers, the formalization treats even and odd dimensions separately: v_{2k} = \pi^k/k! and v_{2k+1} = \pi^k 2^{2k+1}k!/(2k+1)! (CohnElkies.unitBallVolume_odd), and \log(k!)/k - \log k \to -1 (Stirling.tendsto_log_factorial_div_sub_log, from Stirling.tendsto_stirlingSeq_sqrt_pi) gives the same limit along both subsequences (Filter.tendsto_of_even_odd).