tendsto_sum_range_one_div_nat_succ_atTop

English

The sequence of partial sums S_n = ∑_{i=1}^n 1/i diverges to +∞ as n → ∞.

Русский

Последовательность частичных сумм S_n = ∑_{i=1}^n 1/i расходится к +∞ при n → ∞.

LaTeX

$$$$\displaystyle \lim_{n\to\infty} \sum_{i=1}^{n} \frac{1}{i} = +\infty.$$$$

Lean4

/-- **Divergence of the Harmonic Series** -/
theorem tendsto_sum_range_one_div_nat_succ_atTop :
    Tendsto (fun n => ∑ i ∈ Finset.range n, (1 / (i + 1) : ℝ)) atTop atTop :=
  by
  rw [← not_summable_iff_tendsto_nat_atTop_of_nonneg]
  · exact_mod_cast mt (_root_.summable_nat_add_iff 1).1 not_summable_one_div_natCast
  · exact fun i => by positivity

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