Documentation

Mathlib.NumberTheory.Harmonic.Bounds

This file proves log(n+1)Hn1+log(n) for all natural numbers n.

theorem log_add_one_le_harmonic (n : ) :
Real.log (n + 1) (harmonic n)