English
Let x be a unit in a Normed Ring R with HasSummableGeomSeries. Then as t → 0, inverse(x + t) = x^{-1} - x^{-1} t x^{-1} + O(||t||^2).
Русский
Пусть x — единица в нормированном кольце R с суммируемой геометрической геометрией. Тогда при t → 0 выполняется разложение inv(x + t) = x^{-1} - x^{-1} t x^{-1} + O(||t||^2).
LaTeX
$$$(x+t)^{-1} - x^{-1} + x^{-1} t x^{-1} = O(\\|t\\|^2) \\quad \\text{as } t \\to 0$$$
Lean4
/-- The function `fun t ↦ Ring.inverse (x + t) - x⁻¹ + x⁻¹ * t * x⁻¹` is `O(t ^ 2)` as `t → 0`. -/
theorem inverse_add_norm_diff_second_order (x : Rˣ) :
(fun t : R => inverse (↑x + t) - ↑x⁻¹ + ↑x⁻¹ * t * ↑x⁻¹) =O[𝓝 0] fun t => ‖t‖ ^ 2 :=
by
convert inverse_add_norm_diff_nth_order x 2 using 2
simp only [sum_range_succ, sum_range_zero, zero_add, pow_zero, pow_one, add_mul, one_mul, ← sub_sub, neg_mul,
sub_neg_eq_add]
