strictMono_eulerMascheroniSeq — Mathlib

English

Let S be the Euler–Mascheroni sequence. It is strictly increasing: for m > n, S(m) > S(n).

Русский

Пусть S обозначает последовательность Эйлера–Машчерони. Она строго возрастает: если m > n, то S(m) > S(n).

LaTeX

$$$\forall m,n \in \mathbb{N},\ m

Lean4

theorem strictMono_eulerMascheroniSeq : StrictMono eulerMascheroniSeq :=
  by
  refine strictMono_nat_of_lt_succ (fun n ↦ ?_)
  rw [eulerMascheroniSeq, eulerMascheroniSeq, ← sub_pos, sub_sub_sub_comm, harmonic_succ, add_comm, Rat.cast_add,
    add_sub_cancel_right, ← log_div (by positivity) (by positivity), add_div, Nat.cast_add_one, Nat.cast_add_one,
    div_self (by positivity), sub_pos, one_div, Rat.cast_inv, Rat.cast_add, Rat.cast_one, Rat.cast_natCast]
  refine (log_lt_sub_one_of_pos ?_ (ne_of_gt <| lt_add_of_pos_right _ ?_)).trans_le (le_of_eq ?_)
  · positivity
  · positivity
  · simp only [add_sub_cancel_left]

Похожие утверждения