Commit 2026-09-21 13:42 d0a050ad

feat(Analysis/Asymptotics): continuous / analytic functions are IsTheta at a point (#43810) Show that a function which is continuous and non-zero at a point x satisfies f =Θ[𝓝 x] 1, and a function analytic at x₀ is Θ[𝓝 x₀] fun x ↦ (x - x₀)^n for suitable n. In passing we also slightly generalize some existing asymptotics lemmas, allowing the domain to be a NormedAddCommGroup rather than a NormedField.