Algebraic identities and dyadic bounds for harmonic numbers

Elementary order properties, a weighted summation identity, and a base-2 discrete logarithmic upper bound for Mathlib's rational harmonic numbers harmonic : ℕ → ℚ.

Mathlib's Mathlib.NumberTheory.Harmonic.Bounds bounds harmonic n in ℝ by 1 + Real.log n via improper-style interval integrals. Grouping the upper half [⌊n / 2⌋, n) of the harmonic sum gives a purely rational bound harmonic n ≤ Nat.log 2 n + 1 (harmonic_le_log_add_one) with no real analysis dependencies. The weighted sum identity two_mul_sum_add_one_mul_harmonic evaluates the average recursive subproblem cost arising in randomized quicksort and random binary search trees.

Main results

• harmonic_nonneg, harmonic_mono: nonnegativity and monotonicity of harmonic.
• two_mul_sum_add_one_mul_harmonic: 2 * ∑ r ∈ Finset.range m, (r + 1) * harmonic r = m * (m + 1) * harmonic m - m * (m + 3) / 2.
• harmonic_le_log_add_one: harmonic n ≤ Nat.log 2 n + 1 in ℚ.

The dyadic grouping argument is classical; see [CLRS09], Appendix A.2, pp. 1153–1154. The rational half-splitting and weighted-sum induction proofs below are this formalization's adaptations for the word-RAM analysis.

References

• T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, Introduction to Algorithms, Appendix A.2, pp. 1153–1154.

theorem harmonic_nonneg (n : ℕ) : 0 ≤ harmonic n

Every harmonic number is nonnegative.

theorem harmonic_mono : Monotone harmonic

Harmonic numbers are monotone in their index.

theorem two_mul_sum_add_one_mul_harmonic (m : ℕ) : 2 * ∑ r ∈ Finset.range m, (↑r + 1) * harmonic r = ↑m * (↑m + 1) * harmonic m - ↑m * (↑m + 3) / 2

Weighted summation identity 2 ∑_{r < m} (r + 1) H_r = m (m + 1) H_m - m (m + 3) / 2 in ℚ.

theorem harmonic_le_log_add_one (n : ℕ) : harmonic n ≤ ↑(Nat.log 2 n) + 1

Dyadic condensation upper bound H_n ≤ ⌊log₂ n⌋ + 1 in ℚ.