Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-26 16:37 547d67fc

View on Github →

feat(analysis/{analytic,calculus}): an analytic function is strictly differentiable (#5878)

Estimated changes

Modified src/analysis/analytic/basic.lean

added theorem formal_multilinear_series.norm_le_div_pow_of_pos_of_lt_radius

added theorem has_fpower_series_at.is_O_image_sub_norm_mul_norm_sub

added theorem has_fpower_series_on_ball.has_sum_sub

added theorem has_fpower_series_on_ball.image_sub_sub_deriv_le

added theorem has_fpower_series_on_ball.is_O_image_sub_image_sub_deriv_principal

Modified src/analysis/asymptotics.lean

added theorem asymptotics.is_O_principal

added theorem asymptotics.is_O_with_principal

Modified src/analysis/calculus/deriv.lean

added theorem has_fpower_series_at.deriv

added theorem has_fpower_series_at.has_deriv_at

added theorem has_fpower_series_at.has_strict_deriv_at

Modified src/analysis/calculus/fderiv.lean

added theorem analytic_at.differentiable_at

added theorem analytic_at.differentiable_within_at

added theorem has_fpower_series_at.differentiable_at

added theorem has_fpower_series_at.fderiv

added theorem has_fpower_series_at.has_fderiv_at

added theorem has_fpower_series_at.has_strict_fderiv_at

added theorem has_fpower_series_on_ball.differentiable_on

Modified src/data/pi.lean

added theorem pi.div_def

added theorem subsingleton.pi_single_eq