PrimeNumberTheoremAnd

Critical-line Gamma decay: ‖Γ(1/2+iτ)‖ ≤ √(2π) exp(-π|τ|/2).

The Weierstrass bound for the digamma series summand on a bounded substrip of the right half-plane.

The linear-decay bound for the digamma series summand on a right half-plane, used for the head of the series in the growth estimate.

A summable telescoping series whose terms tend to zero sums to its first term.

The tail of the series ∑ 1 / (m + 1) ^ 2 past N is at most 1 / N.

The increment of logGammaSeq in closed form.

For 0 < z.re, the sequence logGammaSeq z is Cauchy.

On the right half-plane, exp (logGammaSeq z n) = GammaSeq z n for n ≠ 0.

The digamma series on the right half-plane.

The series representation of the digamma function: for z away from the poles of Gamma, the series ∑ (1 / (n + 1) - 1 / (n + z)) sums to digamma z + γ, where γ is the Euler-Mascheroni constant.

The digamma function is continuous on bounded closed substrips of the right half-plane.

The digamma function is continuous at every point of the open right half-plane.

The digamma function is differentiable on bounded open substrips of the right half-plane.

The digamma function is differentiable at every point of the open right half-plane.

The digamma function grows at most logarithmically on vertical strips inside the right half-plane: on a ≤ z.re ≤ b with 0 < a, ‖digamma z‖ ≤ C * Real.log (|z.im| + 2).

The growth bound for digamma (w / 2) on vertical strips, the form consumed by explicit-formula contour integrals.

If 0 < a < re s, then subtracting a from s does not increase the norm.

Product bound: |∏_{k < m} (s-1-k)| ≤ |s|^m

Product bound: |∏_{k < m} (s-1-k)| ≤ |s|^m -/ lemma prod_norm_le_pow {s : ℂ} {m : ℕ} (h : ∀ k < m, (k : ℝ) + 1 < s.re) : ‖∏ k ∈ Finset.range m, (s - 1 - k)‖ ≤ ‖s‖ ^ m := by calc ‖∏ k ∈ Finset.range m, (s - 1 - k)‖ = ∏ k ∈ Finset.range m, ‖s - 1 - k‖ := norm_prod _ _ _ ≤ ∏ _k ∈ Finset.range m, ‖s‖ := by apply Finset.prod_le_prod (fun k _ => norm_nonneg _) intro k hk; exact norm_shift_le (h k (Finset.mem_range.mp hk)) _ = ‖s‖ ^ m := by rw [Finset.prod_const, Finset.card_range]

/-! ## Iterated functional equation

For x ∈ [1, 2], Γ(x) ≤ 1 since Γ(1) = Γ(2) = 1 and the function is convex.