Commit 2024-09-17 19:29 60e4a87a

View on Github →

chore: split the change origin part from Analytic.Basic (#16891) Just moving things around, no mathematical change.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Analytic/Basic.lean

deleted theorem AnalyticAt.eventually_analyticAt

deleted theorem AnalyticAt.exists_ball_analyticOn

deleted theorem AnalyticAt.exists_mem_nhds_analyticOn

deleted theorem FormalMultilinearSeries.analyticAt_changeOrigin

deleted def FormalMultilinearSeries.changeOrigin

deleted def FormalMultilinearSeries.changeOriginIndexEquiv

deleted def FormalMultilinearSeries.changeOriginSeries

deleted def FormalMultilinearSeries.changeOriginSeriesTerm

deleted theorem FormalMultilinearSeries.changeOriginSeriesTerm_apply

deleted theorem FormalMultilinearSeries.changeOriginSeriesTerm_changeOriginIndexEquiv_symm

deleted theorem FormalMultilinearSeries.changeOriginSeries_summable_aux₁

deleted theorem FormalMultilinearSeries.changeOriginSeries_summable_aux₂

deleted theorem FormalMultilinearSeries.changeOriginSeries_summable_aux₃

deleted theorem FormalMultilinearSeries.changeOrigin_eval

deleted theorem FormalMultilinearSeries.changeOrigin_radius

deleted def FormalMultilinearSeries.derivSeries

deleted theorem FormalMultilinearSeries.hasFPowerSeriesOnBall_changeOrigin

deleted theorem FormalMultilinearSeries.le_changeOriginSeries_radius

deleted theorem FormalMultilinearSeries.nnnorm_changeOriginSeriesTerm

deleted theorem FormalMultilinearSeries.nnnorm_changeOriginSeriesTerm_apply_le

deleted theorem FormalMultilinearSeries.nnnorm_changeOriginSeries_apply_le_tsum

deleted theorem FormalMultilinearSeries.nnnorm_changeOriginSeries_le_tsum

deleted theorem FormalMultilinearSeries.nnnorm_changeOrigin_le

deleted theorem FormalMultilinearSeries.norm_changeOriginSeriesTerm

deleted theorem HasFPowerSeriesOnBall.analyticAt_of_mem

deleted theorem HasFPowerSeriesOnBall.analyticOn

deleted theorem HasFPowerSeriesOnBall.changeOrigin

deleted theorem isOpen_analyticAt

Modified Mathlib/Analysis/Analytic/CPolynomial.lean

Created Mathlib/Analysis/Analytic/ChangeOrigin.lean

added theorem AnalyticAt.eventually_analyticAt

added theorem AnalyticAt.exists_ball_analyticOn

added theorem AnalyticAt.exists_mem_nhds_analyticOn

added theorem FormalMultilinearSeries.analyticAt_changeOrigin

added def FormalMultilinearSeries.changeOrigin

added def FormalMultilinearSeries.changeOriginIndexEquiv

added def FormalMultilinearSeries.changeOriginSeries

added def FormalMultilinearSeries.changeOriginSeriesTerm

added theorem FormalMultilinearSeries.changeOriginSeriesTerm_apply

added theorem FormalMultilinearSeries.changeOriginSeriesTerm_changeOriginIndexEquiv_symm

added theorem FormalMultilinearSeries.changeOriginSeries_summable_aux₁

added theorem FormalMultilinearSeries.changeOriginSeries_summable_aux₂

added theorem FormalMultilinearSeries.changeOriginSeries_summable_aux₃

added theorem FormalMultilinearSeries.changeOrigin_eval

added theorem FormalMultilinearSeries.changeOrigin_radius

added def FormalMultilinearSeries.derivSeries

added theorem FormalMultilinearSeries.hasFPowerSeriesOnBall_changeOrigin

added theorem FormalMultilinearSeries.le_changeOriginSeries_radius

added theorem FormalMultilinearSeries.nnnorm_changeOriginSeriesTerm

added theorem FormalMultilinearSeries.nnnorm_changeOriginSeriesTerm_apply_le

added theorem FormalMultilinearSeries.nnnorm_changeOriginSeries_apply_le_tsum

added theorem FormalMultilinearSeries.nnnorm_changeOriginSeries_le_tsum

added theorem FormalMultilinearSeries.nnnorm_changeOrigin_le

added theorem FormalMultilinearSeries.norm_changeOriginSeriesTerm

added theorem HasFPowerSeriesOnBall.analyticAt_of_mem

added theorem HasFPowerSeriesOnBall.analyticOn

added theorem HasFPowerSeriesOnBall.changeOrigin

added theorem isOpen_analyticAt

Modified Mathlib/Analysis/Analytic/Uniqueness.lean

Modified Mathlib/Analysis/Normed/Algebra/Exponential.lean