English
For a unit x and natural n, the difference between inverse(x+t) and the nth-order approximation is O(‖t‖^n) as t → 0.
Русский
Для единицы x и натурального n разность между inverse(x+t) и n-ым порядком аппроксимации имеет порядок O(‖t‖^n) при t → 0.
LaTeX
$$$\left(\lambda t. x+t\right)^{-1} - \left(\sum_{i=0}^{n-1}(-x^{-1} t)^i\right) x^{-1} = O\left(\|t\|^n\right) \text{ as } t\to 0$$$
Lean4
/-- The function
`fun t ↦ Ring.inverse (x + t) - (∑ i ∈ Finset.range n, (- x⁻¹ * t) ^ i) * x⁻¹`
is `O(t ^ n)` as `t → 0`. -/
theorem inverse_add_norm_diff_nth_order (x : Rˣ) (n : ℕ) :
(fun t : R => inverse (↑x + t) - (∑ i ∈ range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹) =O[𝓝 (0 : R)] fun t => ‖t‖ ^ n :=
by
refine EventuallyEq.trans_isBigO (.fun_sub (inverse_add_nth_order x n) (.refl _ _)) ?_
simp only [add_sub_cancel_left]
refine ((isBigO_refl _ _).norm_right.mul (inverse_add_norm x)).trans ?_
simp only [mul_one, isBigO_norm_left]
exact ((isBigO_refl _ _).norm_right.const_mul_left _).pow _
