This file defines the harmonic numbers.

• Mathilb/NumberTheory/Harmonic/Int.lean proves that the nth harmonic number is not an integer.
• Mathlib/NumberTheory/Harmonic/Bounds.lean provides basic log bounds.

def harmonic : ℕ → ℚ

The nth-harmonic number defined as a finset sum of consecutive reciprocals.

Equations

• harmonic n = ∑ i ∈ Finset.range n, (↑(i + 1))⁻¹

@[simp]

theorem harmonic_zero : harmonic 0 = 0

@[simp]

theorem harmonic_succ (n : ℕ) : harmonic (n + 1) = harmonic n + (↑(n + 1))⁻¹

theorem harmonic_pos {n : ℕ} (Hn : n ≠ 0) : 0 < harmonic n

theorem harmonic_eq_sum_Icc {n : ℕ} : harmonic n = ∑ i ∈ Finset.Icc 1 n, (↑i)⁻¹