Commit 2023-06-05 12:36 1e3b7db8

View on Github →

feat: port Analysis.Calculus.FDerivAnalytic (#4568)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Calculus/FDerivAnalytic.lean

added theorem AnalyticAt.differentiableAt

added theorem AnalyticAt.differentiableWithinAt

added theorem AnalyticOn.contDiffOn

added theorem AnalyticOn.deriv

added theorem AnalyticOn.differentiableOn

added theorem AnalyticOn.fderiv

added theorem AnalyticOn.iteratedFDeriv

added theorem AnalyticOn.iterated_deriv

added theorem HasFPowerSeriesAt.differentiableAt

added theorem HasFPowerSeriesAt.fderiv_eq

added theorem HasFPowerSeriesAt.hasFDerivAt

added theorem HasFPowerSeriesAt.hasStrictFDerivAt

added theorem HasFPowerSeriesOnBall.differentiableOn

added theorem HasFPowerSeriesOnBall.fderiv

added theorem HasFPowerSeriesOnBall.fderiv_eq

added theorem HasFPowerSeriesOnBall.hasFDerivAt