Commit 2021-07-17 09:38 d4c0a118

View on Github →

refactor(analysis/analytic/basic): refactor change_origin (#8282) Now each term of change_origin is defined as a sum of a formal power series, so it is clear that each term is an analytic function.

Estimated changes

Modified src/analysis/analytic/basic.lean

modified theorem formal_multilinear_series.change_origin_eval

deleted theorem formal_multilinear_series.change_origin_has_sum

added def formal_multilinear_series.change_origin_index_equiv

modified theorem formal_multilinear_series.change_origin_radius

added def formal_multilinear_series.change_origin_series

added theorem formal_multilinear_series.change_origin_series_summable_aux₁

added theorem formal_multilinear_series.change_origin_series_summable_aux₂

added theorem formal_multilinear_series.change_origin_series_summable_aux₃

added def formal_multilinear_series.change_origin_series_term

added theorem formal_multilinear_series.change_origin_series_term_apply

deleted theorem formal_multilinear_series.change_origin_summable_aux1

deleted theorem formal_multilinear_series.change_origin_summable_aux2

deleted theorem formal_multilinear_series.change_origin_summable_aux3

deleted def formal_multilinear_series.change_origin_summable_aux_j

deleted theorem formal_multilinear_series.change_origin_summable_aux_j_injective

deleted theorem formal_multilinear_series.continuous_on

deleted theorem formal_multilinear_series.has_fpower_series_on_ball

added theorem formal_multilinear_series.has_fpower_series_on_ball_change_origin

added theorem formal_multilinear_series.le_change_origin_series_radius

modified theorem formal_multilinear_series.le_radius_of_bound

modified theorem formal_multilinear_series.le_radius_of_bound_nnreal

added theorem formal_multilinear_series.le_radius_of_eventually_le

added theorem formal_multilinear_series.le_radius_of_summable

added theorem formal_multilinear_series.le_radius_of_summable_nnnorm

added theorem formal_multilinear_series.nnnorm_change_origin_le

added theorem formal_multilinear_series.nnnorm_change_origin_series_apply_le_tsum

added theorem formal_multilinear_series.nnnorm_change_origin_series_le_tsum

added theorem formal_multilinear_series.nnnorm_change_origin_series_term

added theorem formal_multilinear_series.nnnorm_change_origin_series_term_apply_le

added theorem formal_multilinear_series.norm_change_origin_series_term

added theorem formal_multilinear_series.summable_nnnorm_mul_pow

added theorem formal_multilinear_series.summable_norm_mul_pow

Modified src/data/real/ennreal.lean

added theorem ennreal.le_of_forall_pos_nnreal_lt

Modified src/data/subtype.lean

added theorem subtype.heq_iff_coe_heq

Modified src/topology/algebra/infinite_sum.lean

added theorem summable.div_const