English
For any n, and t with ‖t‖ < 1, the inverse of 1 − t equals the partial geometric sum up to n minus one plus t^n times the inverse of 1 − t.
Русский
Для любого n и t с ‖t‖ < 1, обратное к 1 − t может быть записано как частичная сумма геометрической прогрессии до n-1 плюс t^n умноженное на обратное к 1 − t.
LaTeX
$$$\text{inverse}(1-t) = \sum_{i=0}^{n-1} t^{i} + t^{n} \text{inverse}(1-t) \quad (‖t‖<1).$$$
Lean4
theorem inverse_one_sub_nth_order' (n : ℕ) {t : R} (ht : ‖t‖ < 1) :
inverse ((1 : R) - t) = (∑ i ∈ range n, t ^ i) + t ^ n * inverse (1 - t) :=
have := _root_.summable_geometric_of_norm_lt_one ht
calc
inverse (1 - t) = ∑' i : ℕ, t ^ i := inverse_one_sub t ht
_ = ∑ i ∈ range n, t ^ i + ∑' i : ℕ, t ^ (i + n) := (this.sum_add_tsum_nat_add _).symm
_ = (∑ i ∈ range n, t ^ i) + t ^ n * inverse (1 - t) := by
simp only [inverse_one_sub t ht, add_comm _ n, pow_add, this.tsum_mul_left]; rfl
