English
In a normed ring with summable geometric series, the inverse of 1 − t is bounded near 0.
Русский
В нормированном кольце с суммируемым геометрическим рядом обратное к 1 − t ограничено около нуля.
LaTeX
$$$\text{inverse}(1-t) = O(1) \text{ as } t \to 0$$$
Lean4
/-- The function `fun t ↦ inverse (x + t)` is O(1) as `t → 0`. -/
theorem inverse_add_norm (x : Rˣ) : (fun t : R => inverse (↑x + t)) =O[𝓝 0] fun _t => (1 : ℝ) :=
by
refine EventuallyEq.trans_isBigO (inverse_add x) (one_mul (1 : ℝ) ▸ ?_)
simp only [← sub_neg_eq_add, ← neg_mul]
have hzero : Tendsto (-(↑x⁻¹ : R) * ·) (𝓝 0) (𝓝 0) := (mulLeft_continuous _).tendsto' _ _ <| mul_zero _
exact (inverse_one_sub_norm.comp_tendsto hzero).mul (isBigO_const_const _ one_ne_zero _)
