geom_sum_Ico_le_of_lt_one — Mathlib

English

If 0 ≤ x < 1, then for all natural n, the sum ∑_{i=m}^{n-1} x^i ≤ x^m/(1 − x).

Русский

Если 0 ≤ x < 1, то для всех натуральных m,n выполняется ∑_{i=m}^{n-1} x^i ≤ x^m/(1 − x).

LaTeX

$$$\\sum_{i=m}^{n-1} x^i \\le \\dfrac{x^m}{1-x}$ при $0\\le x<1$$$

Lean4

theorem geom_sum_Ico_le_of_lt_one (hx : 0 ≤ x) (h'x : x < 1) : ∑ i ∈ Ico m n, x ^ i ≤ x ^ m / (1 - x) :=
  by
  rcases le_or_gt m n with (hmn | hmn)
  · rw [geom_sum_Ico' h'x.ne hmn]
    apply div_le_div₀ (pow_nonneg hx _) _ (sub_pos.2 h'x) le_rfl
    simpa using pow_nonneg hx _
  · rw [Ico_eq_empty, sum_empty]
    · apply div_nonneg (pow_nonneg hx _)
      simpa using h'x.le
    · simpa using hmn.le

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