inverse_one_sub_nth_order — Mathlib

English

For any n, the inverse of 1 − t has the nth-order expansion with the sum of powers of t up to n−1 plus t^n times the inverse of 1−t, holding near 0.

Русский

Для любого n разложение обратного к 1 − t имеет n-й порядок: сумма до n−1 степеней t плюс t^n умноженное на обратное к 1 − t, окрестно 0.

LaTeX

$$$\text{inverse}(1-t) = \sum_{i=0}^{n-1} t^{i} + t^{n} \text{inverse}(1-t) \quad (t\to 0).$$$

Lean4

theorem inverse_one_sub_nth_order (n : ℕ) :
    ∀ᶠ t in 𝓝 0, inverse ((1 : R) - t) = (∑ i ∈ range n, t ^ i) + t ^ n * inverse (1 - t) :=
  Metric.eventually_nhds_iff.2 ⟨1, one_pos, fun t ht ↦ inverse_one_sub_nth_order' n <| by rwa [← dist_zero_right]⟩

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