English
The modified Euler–Mascheroni sequence S' is strictly decreasing: for m < n, S'(m) > S'(n).
Русский
Модифицированная последовательность Эйлера–Машчерони S' строго убывает: для m < n, S'(m) > S'(n).
LaTeX
$$$\forall m eulerMascheroniSeq'(n)$$$
Lean4
theorem strictAnti_eulerMascheroniSeq' : StrictAnti eulerMascheroniSeq' :=
by
refine strictAnti_nat_of_succ_lt (fun n ↦ ?_)
rcases Nat.eq_zero_or_pos n with rfl | hn
· simp [eulerMascheroniSeq']
simp_rw [eulerMascheroniSeq', eq_false_intro hn.ne', reduceCtorEq, if_false]
rw [← sub_pos, sub_sub_sub_comm, harmonic_succ, Rat.cast_add, ← sub_sub, sub_self, zero_sub, sub_eq_add_neg, neg_sub,
← sub_eq_neg_add, sub_pos, ← log_div (by positivity) (by positivity), ← neg_lt_neg_iff, ← log_inv]
refine (log_lt_sub_one_of_pos ?_ ?_).trans_le (le_of_eq ?_)
· positivity
· simp [field]
· simp [field]
