Source indexedlemma · leanprover/lean4:v4.32.0

euler_maclaurin_decreasing

PrimeNumberTheoremAnd.EulerMascheroniBounds · PrimeNumberTheoremAnd/EulerMascheroniBounds.lean:186 to 196

Source documentation

γ₂ is strictly decreasing for n ≥ 1.

Exact Lean statement

lemma euler_maclaurin_decreasing (n : ℕ) (hn : 1 ≤ n) :
    γ₂ (n + 1) < γ₂ n

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma euler_maclaurin_decreasing (n : ℕ) (hn : 1 ≤ n) :    γ₂ (n + 1) < γ₂ n := by  unfold γ₂  suffices h : Real.log ((n + 1 : ℝ) / n) - (2 * n + 1) / (2 * n * (n + 1)) +      (2 * n + 1) / (12 * n ^ 2 * (n + 1) ^ 2) > 0 by    rw [Real.log_div] at h <;> norm_num at * <;> try positivity    field_simp at *; grind  have h_log_ineq : 12 * (1 + 1 / (n : ℝ)) ^ 2 * Real.log (1 + 1 / (n : ℝ)) >      12 / (n : ℝ) + 18 / (n : ℝ) ^ 2 + 4 / (n : ℝ) ^ 3 - 1 / (n : ℝ) ^ 4 := by    have := log_ineq_3 (1 / (n : ℝ)) (by positivity); aesop  field_simp at *; grind