Commit 2024-09-16 00:14 605d02e9

View on Github →

feat: analyticity of functions in pi spaces (#16753)

Estimated changes

Modified Mathlib/Analysis/Analytic/Constructions.lean

added theorem AnalyticAt.pi

added theorem AnalyticOn.pi

added theorem AnalyticWithinAt.pi

added theorem AnalyticWithinOn.pi

added theorem FormalMultilinearSeries.le_radius_pi

added theorem FormalMultilinearSeries.radius_pi_eq_iInf

added theorem FormalMultilinearSeries.radius_pi_le

added theorem HasFPowerSeriesAt.pi

added theorem HasFPowerSeriesOnBall.pi

added theorem HasFPowerSeriesWithinAt.pi

added theorem HasFPowerSeriesWithinOnBall.pi

added theorem hasFPowerSeriesAt_pi_iff

added theorem hasFPowerSeriesOnBall_pi_iff

added theorem hasFPowerSeriesWithinAt_pi_iff

added theorem hasFPowerSeriesWithinOnBall_pi_iff

Modified Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean

added def FormalMultilinearSeries.pi