Commit 2023-10-18 11:36 ea1c5f87

View on Github →

feat(Analysis/Analytic): some more API for analytic functions (#7552) This PR adds some basic results about analytic functions: products of analytic functions are analytic, and the inverse map on a normed field is analytic away from 0.

Estimated changes

Modified Mathlib/Analysis/Analytic/Basic.lean

added theorem AnalyticAt.prod

added theorem AnalyticOn.prod

added theorem FormalMultilinearSeries.radius_prod_eq_min

added theorem HasFPowerSeriesAt.prod

added theorem HasFPowerSeriesOnBall.prod

added theorem analyticAt_inv_one_sub

added theorem formalMultilinearSeries_geometric_radius

added theorem hasFPowerSeriesOnBall_inv_one_sub

Modified Mathlib/Analysis/Analytic/Linear.lean

added theorem AnalyticAt.mul

added theorem AnalyticAt.pow

added theorem AnalyticAt.smul

deleted def ContinuousLinearMap.fpowerSeries

deleted theorem ContinuousLinearMap.fpowerSeries_apply_add_two

deleted theorem ContinuousLinearMap.fpower_series_apply_one

deleted theorem ContinuousLinearMap.fpower_series_apply_zero

added theorem analyticAt_id

added theorem analyticAt_inv

added theorem analyticAt_mul

added theorem analyticAt_smul

Modified Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean

added def ContinuousLinearMap.fpowerSeries

added theorem ContinuousLinearMap.fpowerSeries_apply_add_two

added theorem ContinuousLinearMap.fpower_series_apply_one

added theorem ContinuousLinearMap.fpower_series_apply_zero

added theorem FormalMultilinearSeries.neg_apply

added def FormalMultilinearSeries.prod

added theorem FormalMultilinearSeries.zero_apply

added def formalMultilinearSeries_geometric

added theorem formalMultilinearSeries_geometric_apply_norm

deleted theorem neg_apply

deleted theorem zero_apply