Commit 2020-12-31 16:30 0830bfd4

View on Github →

refactor(analysis/analytic/basic): redefine formal_multilinear_series.radius (#5349) With the new definition, (a) some proofs get much shorter; (b) we don't need rpow in analytic/basic.

Estimated changes

Modified src/algebra/big_operators/order.lean

Modified src/analysis/analytic/basic.lean

deleted theorem formal_multilinear_series.bound_of_lt_radius

modified def formal_multilinear_series.change_origin

deleted theorem formal_multilinear_series.geometric_bound_of_lt_radius

added theorem formal_multilinear_series.is_o_of_lt_radius

added theorem formal_multilinear_series.is_o_one_of_lt_radius

modified theorem formal_multilinear_series.le_radius_of_bound

added theorem formal_multilinear_series.le_radius_of_bound_nnreal

added theorem formal_multilinear_series.le_radius_of_is_O

added theorem formal_multilinear_series.lt_radius_of_is_O

added theorem formal_multilinear_series.nnnorm_mul_pow_le_of_lt_radius

added theorem formal_multilinear_series.norm_mul_pow_le_mul_pow_of_lt_radius

added theorem formal_multilinear_series.norm_mul_pow_le_of_lt_radius

modified theorem formal_multilinear_series.radius_neg

Modified src/analysis/analytic/composition.lean

Created src/analysis/analytic/radius_liminf.lean

added theorem formal_multilinear_series.radius_eq_liminf

Modified src/analysis/specific_limits.lean