log_le_harmonic_floor — Mathlib

English

For y ∈ ℝ with y ≥ 0, log y ≤ harmonic( floor y ) and related inequalities.

Русский

Для y ≥ 0 верно log y ≤ гармоническое число floor(y).

LaTeX

$$$\log y \le \operatorname{harmonic}(\left\lfloor y \right\rfloor)\quad (y>0)$$$

Lean4

theorem log_le_harmonic_floor (y : ℝ) (hy : 0 ≤ y) : Real.log y ≤ harmonic ⌊y⌋₊ :=
  by
  by_cases h0 : y = 0
  · simp [h0]
  · calc
      _ ≤ Real.log ↑(Nat.floor y + 1) := ?_
      _ ≤ _ := log_add_one_le_harmonic _
    gcongr
    apply (Nat.le_ceil y).trans
    norm_cast
    exact Nat.ceil_le_floor_add_one y

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