mul_pow_le_nat_floor_pow — Mathlib

English

For c>1 and i≥0, (1 - c^{-1}) c^i ≤ ⌊c^i⌋.

Русский

Для c>1 и i≥0 выполняется (1 - c^{-1}) c^i ≤ ⌊c^i⌋.

LaTeX

$$$$ (1 - c^{-1}) * c^{i} ≤ ⌊c^{i}⌋_+ $$$$

Lean4

theorem mul_pow_le_nat_floor_pow {c : ℝ} (hc : 1 < c) (i : ℕ) : (1 - c⁻¹) * c ^ i ≤ ⌊c ^ i⌋₊ :=
  by
  have cpos : 0 < c := zero_lt_one.trans hc
  rcases eq_or_ne i 0 with (rfl | hi)
  · simp only [pow_zero, Nat.floor_one, Nat.cast_one, mul_one, sub_le_self_iff, inv_nonneg, cpos.le]
  calc
    (1 - c⁻¹) * c ^ i = c ^ i - c ^ i * c⁻¹ := by ring
    _ ≤ c ^ i - 1 := by
      gcongr
      simpa only [← div_eq_mul_inv, one_le_div cpos, pow_one] using le_self_pow₀ hc.le hi
    _ ≤ ⌊c ^ i⌋₊ := (Nat.sub_one_lt_floor _).le

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