Source indexedlemma · leanprover/lean4:v4.32.0

Complex.Gamma.norm_mul_log_shift_half_bound

PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.StripBounds · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Gamma/StripBounds.lean:162 to 185

Source documentation

For ‖s‖ ≥ 1, the s ↦ s/2 + 1 shift in the half-plane Stirling exponent.

Exact Lean statement

lemma norm_mul_log_shift_half_bound {s : ℂ} (hs : 1 ≤ ‖s‖) :
    ‖s / 2 + 1‖ * Real.log (1 + ‖s / 2 + 1‖) ≤
      Real.Stirling.half_shift_log_constant * (‖s‖ * Real.log (1 + ‖s‖))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma norm_mul_log_shift_half_bound {s : ℂ} (hs : 1 ≤ ‖s‖) :    ‖s / 2 + 1‖ * Real.log (1 + ‖s / 2 + 1‖) ≤      Real.Stirling.half_shift_log_constant * (‖s‖ * Real.log (1 + ‖s‖)) := by  have hlog_nonneg : 0 ≤ Real.log (1 + ‖s / 2 + 1‖) :=    Real.log_nonneg (by linarith [norm_nonneg (s / 2 + 1)])  have hlog_w' :      Real.log (1 + ‖s / 2 + 1‖) ≤        (Real.log 3 / Real.log 2 + 1) * Real.log (1 + ‖s‖) := by    nlinarith [log_one_add_norm_div_two_add_one_le hs,      Real.Stirling.log_three_le_coef_mul_log_one_add hs]  calc    ‖s / 2 + 1‖ * Real.log (1 + ‖s / 2 + 1‖)        ≤ ((3 / 2 : ℝ) * ‖s‖) * Real.log (1 + ‖s / 2 + 1‖) :=          mul_le_mul_of_nonneg_right (norm_div_two_add_one_le_three_halves_mul hs) hlog_nonneg    _ ≤ Real.Stirling.half_shift_log_constant * (‖s‖ * Real.log (1 + ‖s‖)) := by      have hstep2 :          ((3 / 2 : ℝ) * ‖s‖) * Real.log (1 + ‖s / 2 + 1‖) ≤            ((3 / 2 : ℝ) * ‖s‖) * ((Real.log 3 / Real.log 2 + 1) * Real.log (1 + ‖s‖)) :=        mul_le_mul_of_nonneg_left hlog_w' (by positivity)      have hEq :          ((3 / 2 : ℝ) * ‖s‖) * ((Real.log 3 / Real.log 2 + 1) * Real.log (1 + ‖s‖)) =            Real.Stirling.half_shift_log_constant * (‖s‖ * Real.log (1 + ‖s‖)) := by        simp [Real.Stirling.half_shift_log_constant, mul_assoc, mul_left_comm, mul_comm]      exact le_trans hstep2 (by simp [hEq])