Source indexedlemma · leanprover/lean4:v4.32.0

Complex.Gammaℝ.Stirling.norm_cpow_pi_neg_half_le_one

PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.StripBounds · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Gamma/StripBounds.lean:614 to 624

Source documentation

The norm of π^{-s/2} is at most 1 when Re(s) ≥ 0.

Exact Lean statement

lemma norm_cpow_pi_neg_half_le_one {s : ℂ} (hs : 0 ≤ s.re) :
    ‖(Real.pi : ℂ) ^ (-s / 2)‖ ≤ 1

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma norm_cpow_pi_neg_half_le_one {s : ℂ} (hs : 0 ≤ s.re) :    ‖(Real.pi : ℂ) ^ (-s / 2)‖ ≤ 1 := by  have hpi_pos : (0 : ℝ) < Real.pi := Real.pi_pos  rw [Complex.norm_cpow_eq_rpow_re_of_pos hpi_pos]  have h_re : (-s / 2).re = -s.re / 2 := by simp [Complex.neg_re]  rw [h_re]  have h_exp : -s.re / 2 ≤ 0 := by linarith  have hpi_gt_1 : (1 : ℝ) < Real.pi := by    calc (1 : ℝ) < 3 := by norm_num      _ < Real.pi := Real.pi_gt_three  exact Real.rpow_le_one_of_one_le_of_nonpos (le_of_lt hpi_gt_1) h_exp