Commit 2021-01-15 21:05 d43f202f

feat(analysis/analytic/basic): f (x + y) - p.partial_sum n y = O(∥y∥ⁿ) (#5756)

Lemmas about analytic functions

• add has_fpower_series_on_ball.uniform_geometric_approx', a more precise version of has_fpower_series_on_ball.uniform_geometric_approx;
• add has_fpower_series_at.is_O_sub_partial_sum_pow, a version of the Taylor formula for an analytic function;

Lemmas about homeomorph and topological groups

• add simp lemmas homeomorph.coe_mul_left and homeomorph.mul_left_symm;
• add map_mul_left_nhds and map_mul_left_nhds_one;
• add homeomorph.to_equiv_injective and homeomorph.ext;

Lemmas about is_O/is_o

• add simp lemmas asymptotics.is_O_with_map, asymptotics.is_O_map, and asymptotics.is_o_map;
• add asymptotics.is_o_norm_pow_norm_pow and asymptotics.is_o_norm_pow_id;

Misc changes

• rename div_le_iff_of_nonneg_of_le to div_le_of_nonneg_of_le_mul;
• add continuous_linear_map.op_norm_le_of_nhds_zero;
• golf some proofs.