Commit 2024-09-28 07:48 8d426f12

View on Github →

feat: the inverse of an analytic partial homeo is also analytic (#17170) We already have the results for the inverse of formal multilinear series, so this PR is mostly just extending our API. However, this showed that our API is suboptimal (notably with respect to the choice of constant coefficients in inverses of formal multilinear series), so we also tweak the definitions of FormalMultilinearSeries.id and FormalMultilinearSeries.leftInv/rightInv to make them more usable.

Estimated changes

Modified Mathlib/Analysis/Analytic/Basic.lean

added theorem HasFPowerSeriesAt.tendsto_partialSum

Modified Mathlib/Analysis/Analytic/Composition.lean

added theorem FormalMultilinearSeries.compPartialSumTarget_tendsto_prod_atTop

modified theorem FormalMultilinearSeries.comp_id

modified def FormalMultilinearSeries.id

deleted theorem FormalMultilinearSeries.id_apply_ne_one

added theorem FormalMultilinearSeries.id_apply_of_one_lt

modified theorem FormalMultilinearSeries.id_apply_one'

modified theorem FormalMultilinearSeries.id_apply_one

added theorem FormalMultilinearSeries.id_apply_zero

added theorem FormalMultilinearSeries.id_comp'

modified theorem FormalMultilinearSeries.id_comp

Modified Mathlib/Analysis/Analytic/Inverse.lean

modified theorem FormalMultilinearSeries.comp_rightInv

modified theorem FormalMultilinearSeries.comp_rightInv_aux2

modified theorem FormalMultilinearSeries.leftInv_coeff_one

modified theorem FormalMultilinearSeries.leftInv_coeff_zero

modified theorem FormalMultilinearSeries.leftInv_comp

modified theorem FormalMultilinearSeries.leftInv_eq_rightInv

modified theorem FormalMultilinearSeries.leftInv_removeZero

added theorem FormalMultilinearSeries.radius_leftInv_pos_of_radius_pos

modified theorem FormalMultilinearSeries.radius_rightInv_pos_of_radius_pos

modified theorem FormalMultilinearSeries.radius_rightInv_pos_of_radius_pos_aux2

modified theorem FormalMultilinearSeries.rightInv_coeff

modified theorem FormalMultilinearSeries.rightInv_coeff_one

modified theorem FormalMultilinearSeries.rightInv_coeff_zero

modified theorem FormalMultilinearSeries.rightInv_removeZero

added theorem HasFPowerSeriesAt.eventually_hasSum_of_comp

added theorem HasFPowerSeriesAt.tendsto_partialSum_prod_of_comp

added theorem PartialHomeomorph.hasFPowerSeriesAt_symm

Modified Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean

added theorem HasProd.of_sigma