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))⁻¹