one_half_lt_eulerMascheroniSeq_six

English

For the modified Euler–Mascheroni sequence S', the sixth term exceeds one half.

Русский

Для модифицированной последовательности Эйлера–Машчерони S' шестой член превосходит одну половину.

LaTeX

$$$\tfrac{1}{2} < eulerMascheroniSeq'(6)$$$

Lean4

theorem one_half_lt_eulerMascheroniSeq_six : 1 / 2 < eulerMascheroniSeq 6 :=
  by
  have : eulerMascheroniSeq 6 = 49 / 20 - log 7 :=
    by
    rw [eulerMascheroniSeq]
    norm_num
  rw [this, lt_sub_iff_add_lt, ← lt_sub_iff_add_lt', log_lt_iff_lt_exp (by positivity)]
  refine lt_of_lt_of_le ?_ (Real.sum_le_exp_of_nonneg (by norm_num) 7)
  simp_rw [Finset.sum_range_succ, Nat.factorial_succ]
  norm_num

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