Commit 2026-01-06 17:44 e640e393

View on Github →

feat(Analysis/Analytic): analytic order of a composition (#33000) Show that:

The analytic and/or meromorphic order of a function at a point is well-behaved under composition with an analytic function.
Local inverses of analytic functions are analytic.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Analytic/Order.lean

added theorem AnalyticAt.analyticOrderAt_comp

added theorem AnalyticAt.analyticOrderAt_deriv_add_one

added theorem AnalyticAt.analyticOrderAt_sub_eq_one_of_deriv_ne_zero

added theorem analyticOrderAt_comp_of_deriv_ne_zero

added theorem eventuallyConst_iff_analyticOrderAt_sub_eq_top

Modified Mathlib/Analysis/Calculus/FDeriv/Analytic.lean

added theorem AnalyticAt.hasStrictDerivAt

Created Mathlib/Analysis/Calculus/InverseFunctionTheorem/Analytic.lean

added theorem AnalyticAt.analyticAt_localInverse

added theorem analyticAt_comp_iff_of_deriv_ne_zero

Modified Mathlib/Analysis/Calculus/InverseFunctionTheorem/Deriv.lean

added theorem HasStrictDerivAt.eventually_left_inverse

added theorem HasStrictDerivAt.eventually_right_inverse

Modified Mathlib/Analysis/Meromorphic/Basic.lean

added theorem MeromorphicAt.comp_analyticAt

added theorem meromorphicAt_comp_iff_of_deriv_ne_zero

added theorem meromorphicAt_mul_iff_of_ne_zero

added theorem meromorphicAt_smul_iff_of_ne_zero

Modified Mathlib/Analysis/Meromorphic/Order.lean

deleted theorem MeromorphicAt.comp_analyticAt

added theorem MeromorphicAt.meromorphicOrderAt_comp

added theorem eventuallyConst_nhdsNE_iff_meromorphicOrderAt_sub_eq_top

added theorem meromorphicOrderAt_comp_of_deriv_ne_zero

added theorem meromorphicOrderAt_mul_of_ne_zero

added theorem meromorphicOrderAt_smul_of_ne_zero

Modified Mathlib/Data/ENat/Basic.lean

added theorem ENat.map_natCast_mul