English
For all n, harmonic n ≤ 1 + log n, establishing a two-sided control with log.
Русский
Для всех n гармоническое число ≤ 1 + логарифм n, обеспечивая двойной контроль с логарифмом.
LaTeX
$$$\mathrm{harmonic}(n) \le 1 + \log(n) \quad (n\ge 1)$$$
Lean4
theorem harmonic_le_one_add_log (n : ℕ) : harmonic n ≤ 1 + Real.log n :=
by
by_cases hn0 : n = 0
· simp [hn0]
have hn : 1 ≤ n := Nat.one_le_iff_ne_zero.mpr hn0
simp_rw [harmonic_eq_sum_Icc, Rat.cast_sum, Rat.cast_inv, Rat.cast_natCast]
rw [← Finset.sum_erase_add (Finset.Icc 1 n) _ (Finset.left_mem_Icc.mpr hn), add_comm, Nat.cast_one, inv_one]
refine add_le_add_left ?_ 1
simp only [Finset.Icc_erase_left]
calc
∑ d ∈ .Ico 2 (n + 1), (d : ℝ)⁻¹
_ = ∑ d ∈ .Ico 2 (n + 1), (↑(d + 1) - 1)⁻¹ := ?_
_ ≤ ∫ x in 2..↑(n + 1), (x - 1)⁻¹ := ?_
_ = ∫ x in 1..n, x⁻¹ := ?_
_ = Real.log ↑n := ?_
· simp_rw [Nat.cast_add, Nat.cast_one, add_sub_cancel_right]
·
exact
@AntitoneOn.sum_le_integral_Ico 2 (n + 1) (fun x : ℝ ↦ (x - 1)⁻¹) (by linarith [hn]) <|
sub_inv_antitoneOn_Icc_right (by simp)
· convert intervalIntegral.integral_comp_sub_right _ 1
· norm_num
· simp only [Nat.cast_add, Nat.cast_one, add_sub_cancel_right]
· convert integral_inv _
· rw [div_one]
· simp only [Nat.one_le_cast, hn, Set.uIcc_of_le, Set.mem_Icc, Nat.cast_nonneg, and_true, not_le, zero_lt_one]
