Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-01 10:20 16033bb5

View on Github →

feat(analysis/asymptotics,analysis/normed_space/deriv): improvements and additions

Estimated changes

Modified src/analysis/asymptotics.lean

added theorem asymptotics.is_bigo.congr_left

added theorem asymptotics.is_bigo.congr_right

added theorem asymptotics.is_bigo.trans

added theorem asymptotics.is_bigo.trans_is_littleo

added theorem asymptotics.is_bigo_const_mul_left

added theorem asymptotics.is_bigo_const_mul_left_iff

added theorem asymptotics.is_bigo_const_mul_right_iff

added theorem asymptotics.is_bigo_const_one

added theorem asymptotics.is_bigo_const_smul_left

added theorem asymptotics.is_bigo_const_smul_left_iff

added theorem asymptotics.is_bigo_const_smul_right

added theorem asymptotics.is_bigo_iff

deleted theorem asymptotics.is_bigo_iff_pos

added theorem asymptotics.is_bigo_join

added theorem asymptotics.is_bigo_mul

deleted theorem asymptotics.is_bigo_mul_left

deleted theorem asymptotics.is_bigo_mul_right

added theorem asymptotics.is_bigo_of_is_bigo_const_mul_right

deleted theorem asymptotics.is_bigo_of_is_bigo_of_is_bigo

added theorem asymptotics.is_bigo_refl

added theorem asymptotics.is_bigo_smul

deleted theorem asymptotics.is_bigo_smul_left

deleted theorem asymptotics.is_bigo_smul_right

modified theorem asymptotics.is_bigo_zero

added theorem asymptotics.is_bigo_zero_right_iff

added theorem asymptotics.is_littleo.congr_left

added theorem asymptotics.is_littleo.congr_right

added theorem asymptotics.is_littleo.trans

added theorem asymptotics.is_littleo.trans_is_bigo

added theorem asymptotics.is_littleo_const_mul_left

added theorem asymptotics.is_littleo_const_mul_left_iff

added theorem asymptotics.is_littleo_const_mul_right

added theorem asymptotics.is_littleo_const_smul_left

added theorem asymptotics.is_littleo_const_smul_left_iff

added theorem asymptotics.is_littleo_const_smul_right

deleted theorem asymptotics.is_littleo_iff_pos

added theorem asymptotics.is_littleo_join

added theorem asymptotics.is_littleo_mul

modified theorem asymptotics.is_littleo_mul_left

modified theorem asymptotics.is_littleo_mul_right

deleted theorem asymptotics.is_littleo_of_is_bigo_of_is_littleo

added theorem asymptotics.is_littleo_of_is_littleo_const_mul_right

deleted theorem asymptotics.is_littleo_of_is_littleo_of_is_bigo

deleted theorem asymptotics.is_littleo_of_tendsto

added theorem asymptotics.is_littleo_one_iff

added theorem asymptotics.is_littleo_smul

deleted theorem asymptotics.is_littleo_smul_left

deleted theorem asymptotics.is_littleo_smul_right

modified theorem asymptotics.is_littleo_zero

added theorem asymptotics.is_littleo_zero_right_iff

modified theorem asymptotics.tendsto_nhds_zero_of_is_littleo

Modified src/analysis/normed_space/bounded_linear_maps.lean

modified def is_bounded_linear_map.to_linear_map

Modified src/analysis/normed_space/deriv.lean

modified theorem chain_rule

added theorem chain_rule_at_within

added theorem continuous_at_of_has_fderiv_at

added theorem continuous_at_within_of_has_fderiv_at_within

deleted theorem continuous_of_has_fderiv

deleted theorem has_fderiv_add

added theorem has_fderiv_at.congr

added theorem has_fderiv_at.is_littleo

added theorem has_fderiv_at_add

added theorem has_fderiv_at_const

added theorem has_fderiv_at_id

added theorem has_fderiv_at_iff_tendsto

added theorem has_fderiv_at_neg

added theorem has_fderiv_at_smul

added theorem has_fderiv_at_sub

modified theorem has_fderiv_at_within.congr

added theorem has_fderiv_at_within.mono

added theorem has_fderiv_at_within_add

added theorem has_fderiv_at_within_const

added theorem has_fderiv_at_within_equiv_aux

added theorem has_fderiv_at_within_id

added theorem has_fderiv_at_within_iff_tendsto

deleted def has_fderiv_at_within_mono

added theorem has_fderiv_at_within_neg

added theorem has_fderiv_at_within_of_has_fderiv_at

added theorem has_fderiv_at_within_smul

added theorem has_fderiv_at_within_sub

deleted theorem has_fderiv_const

deleted theorem has_fderiv_equiv_aux

deleted theorem has_fderiv_id

deleted theorem has_fderiv_iff_littleo

deleted theorem has_fderiv_neg

deleted theorem has_fderiv_smul

deleted theorem has_fderiv_sub

Modified src/topology/basic.lean