ofDigitsTerm_le — Mathlib

English

Each term ofDigitsTerm is bounded above by (b-1)·b^{-(n+1)}.

Русский

Каждый член ofDigitsTerm ограничен сверху величиной (b-1)·b^{-(n+1)}.

LaTeX

$$$\mathrm{Real.ofDigitsTerm}(\text{digits})\;n \le \bigl( b - 1 \bigr) \cdot (b : \mathbb{R})^{-(n+1)}$$$

Lean4

theorem ofDigitsTerm_le {b : ℕ} {digits : ℕ → Fin b} {n : ℕ} :
    ofDigitsTerm digits n ≤ (b - 1) * ((b : ℝ) ^ (n + 1))⁻¹ :=
  by
  obtain ⟨c, rfl⟩ := Nat.exists_add_one_eq.mpr (b_pos digits)
  unfold ofDigitsTerm
  gcongr
  simp
  grind

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