geom_sum_lt — Mathlib

English

For x ≠ 0 with x < 1, the partial sums ∑_{i=0}^{n-1} x^i are strictly less than (1 − x)^(-1).

Русский

При x ≠ 0 и x < 1 частичные суммы ∑_{i=0}^{n-1} x^i строго меньше (1 − x)^{-1}.

LaTeX

$$$\\sum_{i=0}^{n-1} x^i < (1-x)^{-1}$, при $x\\neq 0$ и $x<1$$$

Lean4

theorem geom_sum_lt (h0 : x ≠ 0) (h1 : x < 1) (n : ℕ) : ∑ i ∈ range n, x ^ i < (1 - x)⁻¹ :=
  by
  rw [← pos_iff_ne_zero] at h0
  rw [geom_sum_of_lt_one h1, div_lt_iff₀, inv_mul_cancel₀, tsub_lt_self_iff]
  · exact ⟨h0.trans h1, pow_pos h0 n⟩
  · rwa [ne_eq, tsub_eq_zero_iff_le, not_le]
  · rwa [tsub_pos_iff_lt]

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