Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-19 09:54 8bf24777

View on Github →

feat(analysis/asymptotics): prove that a function has derivative 0 using asymptotics (#16934)

From the sphere eversion project
Needed for computing derivatives of the parametric interval integral Co-authored by: Patrick Massot patrickmassot@free.fr

Estimated changes

Modified src/analysis/asymptotics/asymptotics.lean

added theorem asymptotics.is_O.eq_zero_of_norm_pow

added theorem asymptotics.is_O.eq_zero_of_norm_pow_within

added theorem asymptotics.is_O.of_bound'

added theorem asymptotics.is_o_pow_sub_pow_sub

added theorem asymptotics.is_o_pow_sub_sub

added theorem filter.eventually.is_O

added theorem filter.eventually.trans_is_O

Modified src/analysis/calculus/fderiv.lean

added theorem asymptotics.is_O.has_fderiv_at

added theorem asymptotics.is_O.has_fderiv_within_at

added theorem has_fderiv_at.is_O

added theorem has_fderiv_within_at.is_O

Modified src/analysis/normed/field/basic.lean

added theorem real.le_norm_self