harmonic_floor_le_one_add_log — Mathlib

English

For y ∈ ℝ with y ≥ 1, harmonic(floor y) ≤ 1 + log y.

Русский

Для y ≥ 1, harmonic( floor y ) ≤ 1 + log y.

LaTeX

$$$\operatorname{harmonic}(\left\lfloor y \right\rfloor) \le 1 + \log y \quad (y \ge 1)$$$

Lean4

theorem harmonic_floor_le_one_add_log (y : ℝ) (hy : 1 ≤ y) : harmonic ⌊y⌋₊ ≤ 1 + Real.log y :=
  by
  refine (harmonic_le_one_add_log _).trans ?_
  gcongr
  · exact_mod_cast Nat.floor_pos.mpr hy
  · exact Nat.floor_le <| zero_le_one.trans hy

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