log_add_one_le_harmonic — Mathlib

English

The natural log of an integer is bounded above by the harmonic numbers, via integrals and sums.

Русский

Натуральный логарифм числа не выше гармонических чисел, устанавливается через интегралы и суммы.

LaTeX

$$$\log(n) \le \operatorname{harmonic}(n) \quad (n\ge 1)$$$

Lean4

theorem log_add_one_le_harmonic (n : ℕ) : Real.log ↑(n + 1) ≤ harmonic n :=
  by
  calc
    _ = ∫ x in (1 : ℕ)..↑(n + 1), x⁻¹ := ?_
    _ ≤ ∑ d ∈ Finset.Icc 1 n, (d : ℝ)⁻¹ := ?_
    _ = harmonic n := ?_
  · rw [Nat.cast_one, integral_inv (by simp [(show ¬(1 : ℝ) ≤ 0 by simp)]), div_one]
  · exact (inv_antitoneOn_Icc_right <| by simp).integral_le_sum_Ico (Nat.le_add_left 1 n)
  · simp only [harmonic_eq_sum_Icc, Rat.cast_sum, Rat.cast_inv, Rat.cast_natCast]

Похожие утверждения