Commit 2023-06-01 16:20 f7b45073

View on Github →

feat: port Analysis.Analytic.Basic (#4275)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Analytic/Basic.lean

added theorem AnalyticAt.add

added theorem AnalyticAt.neg

added theorem AnalyticAt.sub

added def AnalyticAt

added theorem AnalyticOn.add

added theorem AnalyticOn.mono

added theorem AnalyticOn.sub

added def AnalyticOn

added theorem Asymptotics.IsBigO.continuousMultilinearMap_apply_eq_zero

added theorem ContinuousLinearMap.comp_analyticOn

added theorem ContinuousLinearMap.comp_hasFPowerSeriesOnBall

added def FormalMultilinearSeries.changeOrigin

added def FormalMultilinearSeries.changeOriginIndexEquiv

added def FormalMultilinearSeries.changeOriginSeries

added def FormalMultilinearSeries.changeOriginSeriesTerm

added theorem FormalMultilinearSeries.changeOriginSeriesTerm_apply

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 theorem FormalMultilinearSeries.constFormalMultilinearSeries_radius

added theorem FormalMultilinearSeries.hasFPowerSeriesOnBall_changeOrigin

added theorem FormalMultilinearSeries.isLittleO_of_lt_radius

added theorem FormalMultilinearSeries.isLittleO_one_of_lt_radius

added theorem FormalMultilinearSeries.le_changeOriginSeries_radius

added theorem FormalMultilinearSeries.le_mul_pow_of_radius_pos

added theorem FormalMultilinearSeries.le_radius_of_bound

added theorem FormalMultilinearSeries.le_radius_of_bound_nnreal

added theorem FormalMultilinearSeries.le_radius_of_eventually_le

added theorem FormalMultilinearSeries.le_radius_of_isBigO

added theorem FormalMultilinearSeries.le_radius_of_summable

added theorem FormalMultilinearSeries.le_radius_of_summable_nnnorm

added theorem FormalMultilinearSeries.le_radius_of_summable_norm

added theorem FormalMultilinearSeries.le_radius_of_tendsto

added theorem FormalMultilinearSeries.lt_radius_of_isBigO

added theorem FormalMultilinearSeries.min_radius_le_radius_add

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.nnnorm_mul_pow_le_of_lt_radius

added theorem FormalMultilinearSeries.norm_changeOriginSeriesTerm

added theorem FormalMultilinearSeries.norm_le_div_pow_of_pos_of_lt_radius

added theorem FormalMultilinearSeries.norm_mul_pow_le_mul_pow_of_lt_radius

added theorem FormalMultilinearSeries.norm_mul_pow_le_of_lt_radius

added theorem FormalMultilinearSeries.not_summable_norm_of_radius_lt_nnnorm

added def FormalMultilinearSeries.partialSum

added theorem FormalMultilinearSeries.partialSum_continuous

added def FormalMultilinearSeries.radius

added theorem FormalMultilinearSeries.radius_eq_top_iff_summable_norm

added theorem FormalMultilinearSeries.radius_eq_top_of_eventually_eq_zero

added theorem FormalMultilinearSeries.radius_eq_top_of_forall_image_add_eq_zero

added theorem FormalMultilinearSeries.radius_eq_top_of_forall_nnreal_isBigO

added theorem FormalMultilinearSeries.radius_eq_top_of_summable_norm

added theorem FormalMultilinearSeries.radius_le_radius_continuousLinearMap_comp

added theorem FormalMultilinearSeries.radius_neg

added theorem FormalMultilinearSeries.summable_nnnorm_mul_pow

added theorem FormalMultilinearSeries.summable_norm_apply

added theorem FormalMultilinearSeries.summable_norm_mul_pow

added theorem HasFPowerSeriesAt.add

added theorem HasFPowerSeriesAt.analyticAt

added theorem HasFPowerSeriesAt.apply_eq_zero

added theorem HasFPowerSeriesAt.coeff_zero

added theorem HasFPowerSeriesAt.congr

added theorem HasFPowerSeriesAt.eq_formalMultilinearSeries

added theorem HasFPowerSeriesAt.eq_formalMultilinearSeries_of_eventually

added theorem HasFPowerSeriesAt.eq_zero

added theorem HasFPowerSeriesAt.eq_zero_of_eventually

added theorem HasFPowerSeriesAt.eventually_eq_zero

added theorem HasFPowerSeriesAt.eventually_hasSum

added theorem HasFPowerSeriesAt.eventually_hasSum_sub

added theorem HasFPowerSeriesAt.isBigO_image_sub_norm_mul_norm_sub

added theorem HasFPowerSeriesAt.isBigO_sub_partialSum_pow

added theorem HasFPowerSeriesAt.neg

added theorem HasFPowerSeriesAt.radius_pos

added theorem HasFPowerSeriesAt.sub

added def HasFPowerSeriesAt

added theorem HasFPowerSeriesOnBall.add

added theorem HasFPowerSeriesOnBall.analyticAt

added theorem HasFPowerSeriesOnBall.analyticAt_of_mem

added theorem HasFPowerSeriesOnBall.analyticOn

added theorem HasFPowerSeriesOnBall.changeOrigin

added theorem HasFPowerSeriesOnBall.coeff_zero

added theorem HasFPowerSeriesOnBall.comp_sub

added theorem HasFPowerSeriesOnBall.congr

added theorem HasFPowerSeriesOnBall.eventually_eq_zero

added theorem HasFPowerSeriesOnBall.eventually_hasSum

added theorem HasFPowerSeriesOnBall.eventually_hasSum_sub

added theorem HasFPowerSeriesOnBall.exchange_radius

added theorem HasFPowerSeriesOnBall.hasFPowerSeriesAt

added theorem HasFPowerSeriesOnBall.hasSum_sub

added theorem HasFPowerSeriesOnBall.image_sub_sub_deriv_le

added theorem HasFPowerSeriesOnBall.isBigO_image_sub_image_sub_deriv_principal

added theorem HasFPowerSeriesOnBall.mono

added theorem HasFPowerSeriesOnBall.neg

added theorem HasFPowerSeriesOnBall.r_eq_top_of_exists

added theorem HasFPowerSeriesOnBall.radius_pos

added theorem HasFPowerSeriesOnBall.sub

added theorem HasFPowerSeriesOnBall.sum

added theorem HasFPowerSeriesOnBall.tendstoLocallyUniformlyOn'

added theorem HasFPowerSeriesOnBall.tendstoLocallyUniformlyOn

added theorem HasFPowerSeriesOnBall.tendstoUniformlyOn'

added theorem HasFPowerSeriesOnBall.tendstoUniformlyOn

added theorem HasFPowerSeriesOnBall.uniform_geometric_approx'

added theorem HasFPowerSeriesOnBall.uniform_geometric_approx

added structure HasFPowerSeriesOnBall

added theorem analyticAt_const

added theorem analyticOn_const

added theorem hasFPowerSeriesAt_const

added theorem hasFPowerSeriesAt_iff'

added theorem hasFPowerSeriesAt_iff

added theorem hasFPowerSeriesOnBall_const

added theorem isOpen_analyticAt

Modified Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean

added theorem neg_apply