Source indexedtheorem · leanprover/lean4:v4.32.0

Complex.gamma_half_vertical_norm_le_exp

PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.CriticalLineDecay · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Gamma/CriticalLineDecay.lean:94 to 106

Source documentation

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

Exact Lean statement

theorem gamma_half_vertical_norm_le_exp (τ : ℝ) :
    ‖Complex.Gamma (((1 / 2 : ℝ) : ℂ) + (τ : ℂ) * I)‖ ≤
      Real.sqrt (2 * Real.pi) * Real.exp (-(Real.pi * |τ| / 2))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem gamma_half_vertical_norm_le_exp (τ : ℝ) :    ‖Complex.Gamma (((1 / 2 : ℝ) : ℂ) + (τ : ℂ) * I)‖ ≤      Real.sqrt (2 * Real.pi) * Real.exp (-(Real.pi * |τ| / 2)) := by  refine (sq_le_sq₀ (norm_nonneg _) ?_).mp ?_  · positivity  have hrhs_sq :      (Real.sqrt (2 * Real.pi) * Real.exp (-(Real.pi * |τ| / 2))) ^ 2 =        2 * Real.pi * Real.exp (-(Real.pi * |τ|)) := by    rw [mul_pow, Real.sq_sqrt (by positivity)]    rw [sq, ← Real.exp_add]    ring_nf  rw [hrhs_sq]  exact gamma_half_vertical_norm_sq_le_exp τ