Commit 2024-09-15 18:40 36b6e277

View on Github →

feat: drop completeness assumption for composition of analytic functions within sets (#16752)

Estimated changes

Modified Mathlib/Analysis/Analytic/Basic.lean

added theorem HasFPowerSeriesOnBall.tendsto_partialSum

added theorem HasFPowerSeriesOnBall.tendsto_partialSum_prod

added theorem HasFPowerSeriesWithinOnBall.tendsto_partialSum

added theorem HasFPowerSeriesWithinOnBall.tendsto_partialSum_prod

Modified Mathlib/Analysis/Analytic/Composition.lean

added theorem AnalyticAt.comp_analyticWithinAt

added theorem AnalyticAt.comp_analyticWithinAt_of_eq

added theorem AnalyticOn.comp_analyticWithinOn

added theorem AnalyticWithinAt.comp

added theorem AnalyticWithinAt.comp_of_eq

added theorem AnalyticWithinOn.comp

added theorem HasFPowerSeriesWithinAt.comp

Modified Mathlib/Analysis/Analytic/Within.lean

deleted theorem AnalyticWithinAt.comp

deleted theorem AnalyticWithinOn.comp

Modified Mathlib/Geometry/Manifold/AnalyticManifold.lean