A regularized reciprocal

The functions x ↦ x / (x² + ε) converge pointwise to the totalized reciprocal as positive ε tends to zero. Unlike the reciprocal, each regularizing function is continuous everywhere. This limit is useful for regularizing inverses through functional calculus, including at zero.

theorem Real.tendsto_div_sq_add_nhdsGT_zero (x : ℝ) : Filter.Tendsto (fun (ε : ℝ) => x / (x ^ 2 + ε)) (nhdsWithin 0 (Set.Ioi 0)) (nhds x⁻¹)

As positive ε tends to zero, x / (x² + ε) tends to x⁻¹, also when x = 0.