term_sum_one — Mathlib

English

For N a natural number, term_sum(1,N) = log(N+1) - harmonic(N+1) + 1.

Русский

Для натурального N верно term_sum(1,N) = ln(N+1) - H_{N+1} + 1.

LaTeX

$$$\\\\operatorname{term\\_sum}(1,N) = \\\\log(N+1) - H_{N+1} + 1$$$

Lean4

theorem term_sum_one (N : ℕ) : term_sum 1 N = log (N + 1) - harmonic (N + 1) + 1 := by
  induction N with
  | zero =>
    simp_rw [term_sum, Finset.sum_range_zero, harmonic_succ, harmonic_zero, Nat.cast_zero, zero_add, Nat.cast_one,
      inv_one, Rat.cast_one, log_one, sub_add_cancel]
  | succ N hN =>
    unfold term_sum at hN ⊢
    rw [Finset.sum_range_succ, hN, harmonic_succ (N + 1), term_one (by positivity : 0 < N + 1)]
    push_cast
    ring_nf

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