geo_series_const — Mathlib

English

Constant factor multiplies a convergent geometric series still converges in CauSeq sense.

Русский

Постоянный множитель сохраняет сходящуюся геометрическую серию в CauSeq.

LaTeX

$$$IsCauSeq(abs, \sum a\cdot x^n) \Rightarrow IsCauSeq(abs, \sum a\cdot x^n)$$$

Lean4

theorem geo_series_const (a : α) {x : α} (hx1 : |x| < 1) : IsCauSeq abs fun m ↦ ∑ n ∈ range m, (a * x ^ n) := by
  simpa [mul_sum, Pi.mul_def] using (const a).mul (geo_series x hx1)

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