summable_geometric_iff_norm_lt_one

English

A geometric series ∑ ξ^n is summable in a normed division ring if and only if the norm of ξ is less than one.

Русский

Суммируемость геометрической серии ∑ ξ^n в нормированном кольце эквивалентна тому, что ∥ξ∥ < 1.

LaTeX

$$(Summable (fun n => ξ^n)) ↔ ∥ξ∥ < 1$$

Lean4

/-- A geometric series in a normed field is summable iff the norm of the common ratio is less than
one. -/
@[simp]
theorem summable_geometric_iff_norm_lt_one : (Summable fun n : ℕ ↦ ξ ^ n) ↔ ‖ξ‖ < 1 :=
  by
  refine ⟨fun h ↦ ?_, summable_geometric_of_norm_lt_one⟩
  obtain ⟨k : ℕ, hk : dist (ξ ^ k) 0 < 1⟩ := (h.tendsto_cofinite_zero.eventually (ball_mem_nhds _ zero_lt_one)).exists
  simp only [norm_pow, dist_zero_right] at hk
  rw [← one_pow k] at hk
  exact lt_of_pow_lt_pow_left₀ _ zero_le_one hk

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