natLog_le_logb — Mathlib

English

For natural a and b, the discrete (Nat) logarithm is less than or equal to the real logarithm with base b after identifying naturals with reals.

Русский

Для натуральных a и b дискретный логарифм не превосходит действительный логарифм по основанию b после конвертации натуралов в действительные числа.

LaTeX

$$$(\mathrm{Nat.log}\ b\ a) \le \logb b a$$$

Lean4

theorem natLog_le_logb (a b : ℕ) : Nat.log b a ≤ Real.logb b a :=
  by
  apply le_trans _ (Int.floor_le ((b : ℝ).logb a))
  rw [Real.floor_logb_natCast (Nat.cast_nonneg a), Int.log_natCast, Int.cast_natCast]

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