Source indexedlemma · leanprover/lean4:v4.32.0

eulerMascheroniSeq_diff_lb

PrimeNumberTheoremAnd.EulerMascheroniBounds · PrimeNumberTheoremAnd/EulerMascheroniBounds.lean:82 to 96

Source documentation

For m ≥ n, the difference of Euler-Mascheroni sequence values is bounded below by a telescoping sum.

Exact Lean statement

lemma eulerMascheroniSeq_diff_lb (n m : ℕ) (h : n ≤ m) :
    (1 : ℝ) / (2 * (n + 1)) - 1 / (2 * (m + 1)) ≤
    eulerMascheroniSeq m - eulerMascheroniSeq n

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma eulerMascheroniSeq_diff_lb (n m : ℕ) (h : n ≤ m) :    (1 : ℝ) / (2 * (n + 1)) - 1 / (2 * (m + 1)) ≤    eulerMascheroniSeq m - eulerMascheroniSeq n := by  induction h with  | refl => norm_num  | @step k _ hk =>    have h_step : eulerMascheroniSeq (k + 1) - eulerMascheroniSeq k ≥        1 / (2 * (k + 1) * (k + 2) : ℝ) :=      eulerMascheroniSeq_step_lb k    norm_num [Nat.cast_add_one_ne_zero] at *    nlinarith [inv_pos.mpr (by positivity : 0 < (k : ℝ) + 1),      inv_pos.mpr (by positivity : 0 < (k : ℝ) + 2),      mul_inv_cancel₀ (by positivity : (k : ℝ) + 1 ≠ 0),      mul_inv_cancel₀ (by positivity : (k : ℝ) + 2 ≠ 0),      mul_inv_cancel₀ (by positivity : (k : ℝ) + 1 + 1 ≠ 0)]