Documentation

Mathlib.NumberTheory.Padics.Harmonic

The nth Harmonic number is not an integer. We formalize the proof using 2-adic valuations. This proof is due to Kürschák.

Reference: https://kconrad.math.uconn.edu/blurbs/gradnumthy/padicharmonicsum.pdf

source
def harmonic :
ℕ → ℚ

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

Equations
Instances For
    source
    @[simp]
    theorem harmonic_zero :
    harmonic 0 = 0
    source
    @[simp]
    theorem harmonic_succ (n : ℕ) :
    harmonic (n + 1) = harmonic n + (↑(n + 1))⁻¹
    source
    theorem harmonic_pos {n : ℕ} (Hn : n ≠ 0) :
    0 < harmonic n
    source
    theorem padicValRat_two_harmonic (n : ℕ) :
    padicValRat 2 (harmonic n) = -↑(Nat.log 2 n)

    The 2-adic valuation of the n-th harmonic number is the negative of the logarithm of n.

    source
    theorem padicNorm_two_harmonic {n : ℕ} (hn : n ≠ 0) :
    ‖↑(harmonic n)‖ = 2 ^ Nat.log 2 n

    The 2-adic norm of the n-th harmonic number is 2 raised to the logarithm of n in base 2.

    source
    theorem harmonic_not_int {n : ℕ} (h : 2 ≤ n) :
    ¬Rat.isInt (harmonic n) = true

    The n-th harmonic number is not an integer for n ≥ 2.