Commit 2024-09-27 18:54 7da2960d

View on Github →

feat: expand API around analytic functions (#16985) More basic lemmas for analytic functions (especially versions for AnalyticOn of lemmas we already have for AnalyticOnNhd).

Estimated changes

Modified Mathlib/Analysis/Analytic/Basic.lean

added theorem AnalyticWithinAt.mono_of_mem

added theorem ContinuousLinearMap.comp_analyticOn

added theorem ContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall

added theorem FormalMultilinearSeries.radius_le_of_le

added theorem HasFPowerSeriesWithinAt.mono_of_mem

added theorem HasFPowerSeriesWithinOnBall.congr'

added theorem HasFPowerSeriesWithinOnBall.sum

added theorem analyticWithinAt_insert

added theorem hasFPowerSeriesWithinAt_insert

added theorem hasFPowerSeriesWithinOnBall_insert_self

Modified Mathlib/Analysis/Analytic/ChangeOrigin.lean

added theorem FormalMultilinearSeries.radius_le_radius_derivSeries

added theorem HasFPowerSeriesWithinOnBall.analyticOn

added theorem HasFPowerSeriesWithinOnBall.analyticWithinAt_of_mem

added theorem HasFPowerSeriesWithinOnBall.changeOrigin