Source indexedlemma · leanprover/lean4:v4.32.0

Complex.Gamma.norm_mul_log_shift_add_one_bound

PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.StripBounds · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Gamma/StripBounds.lean:146 to 159

Source documentation

For ‖s‖ ≥ 1, the s ↦ s + 1 shift in the Stirling exponent is absorbed by a factor 4.

Exact Lean statement

lemma norm_mul_log_shift_add_one_bound {s : ℂ} (hs : 1 ≤ ‖s‖) :
    ‖s + 1‖ * Real.log (1 + ‖s + 1‖) ≤ 4 * (‖s‖ * Real.log (1 + ‖s‖))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma norm_mul_log_shift_add_one_bound {s : ℂ} (hs : 1 ≤ ‖s‖) :    ‖s + 1‖ * Real.log (1 + ‖s + 1‖) ≤ 4 * (‖s‖ * Real.log (1 + ‖s‖)) := by  have hlog2_le := Real.Stirling.log_one_add_ge_log_two hs  have hlog_add_le : Real.log (1 + ‖s + 1‖) ≤ 2 * Real.log (1 + ‖s‖) := by    nlinarith [log_one_add_norm_add_one_le hs, hlog2_le]  have hlog_nonneg : 0 ≤ Real.log (1 + ‖s + 1‖) :=    Real.log_nonneg (by linarith [norm_nonneg (s + 1)])  calc    ‖s + 1‖ * Real.log (1 + ‖s + 1‖)        ≤ (2 * ‖s‖) * Real.log (1 + ‖s + 1‖) :=          mul_le_mul_of_nonneg_right (norm_add_one_le_two_mul_norm hs) hlog_nonneg    _ ≤ (2 * ‖s‖) * (2 * Real.log (1 + ‖s‖)) :=          mul_le_mul_of_nonneg_left hlog_add_le (by positivity)    _ = 4 * (‖s‖ * Real.log (1 + ‖s‖)) := by ring