English
Geometric series convergence criterion for general ring β with abs into α.
Русский
Критерий сходящегося геометрического ряда для кольца β с абс(abs).
LaTeX
$$$IsCauSeq.geo_series$$$
Lean4
theorem geo_series [Nontrivial β] (x : β) (hx1 : abv x < 1) : IsCauSeq abv fun n ↦ ∑ m ∈ range n, x ^ m :=
by
have hx1' : abv x ≠ 1 := fun h ↦ by simp [h] at hx1
refine of_abv ?_
simp only [abv_pow abv, geom_sum_eq hx1']
conv in _ / _ => rw [← neg_div_neg_eq, neg_sub, neg_sub]
have : 0 < 1 - abv x := sub_pos.2 hx1
refine of_mono_bounded _ (a := (1 : α) / (1 - abv x)) (m := 0) ?_ ?_
· intro n _
rw [abs_of_nonneg]
· gcongr
exact sub_le_self _ (abv_pow abv x n ▸ abv_nonneg _ _)
refine div_nonneg (sub_nonneg.2 ?_) (sub_nonneg.2 <| le_of_lt hx1)
exact pow_le_one₀ (by positivity) hx1.le
· intro n _
rw [← one_mul (abv x ^ n), pow_succ']
gcongr
