not_summable_natCast_inv — Mathlib

English

The harmonic series ∑_{n≥1} n^{-1} is not summable (does not converge).

Русский

Гармонический ряд ∑_{n≥1} 1/n не суммируемой (не сходится).

LaTeX

$$$$\displaystyle \sum_{n=1}^{\infty} \frac{1}{n} \text{ diverges}.$$$

Lean4

/-- Harmonic series is not unconditionally summable. -/
theorem not_summable_natCast_inv : ¬Summable (fun n => n⁻¹ : ℕ → ℝ) :=
  by
  have : ¬Summable (fun n => ((n : ℝ) ^ 1)⁻¹ : ℕ → ℝ) := mt (summable_nat_pow_inv (p := 1)).1 (lt_irrefl 1)
  simpa

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