Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-01 10:20 5dd1ba58

View on Github →

feat(analysis/*): is_bigo -> is_O, is_littleo -> is_o

Estimated changes

Modified src/analysis/asymptotics.lean

added theorem asymptotics.is_O.add

added theorem asymptotics.is_O.comp

added theorem asymptotics.is_O.congr

added theorem asymptotics.is_O.congr_left

added theorem asymptotics.is_O.congr_of_sub

added theorem asymptotics.is_O.congr_right

added theorem asymptotics.is_O.mono

added theorem asymptotics.is_O.sub

added theorem asymptotics.is_O.symm

added theorem asymptotics.is_O.trans

added theorem asymptotics.is_O.trans_is_o

added theorem asymptotics.is_O.trans_tendsto

added theorem asymptotics.is_O.tri

added def asymptotics.is_O

added theorem asymptotics.is_O_comm

added theorem asymptotics.is_O_congr

added theorem asymptotics.is_O_congr_left

added theorem asymptotics.is_O_congr_right

added theorem asymptotics.is_O_const_mul_left

added theorem asymptotics.is_O_const_mul_left_iff

added theorem asymptotics.is_O_const_mul_right_iff

added theorem asymptotics.is_O_const_one

added theorem asymptotics.is_O_const_smul_left

added theorem asymptotics.is_O_const_smul_left_iff

added theorem asymptotics.is_O_const_smul_right

added theorem asymptotics.is_O_iff

added theorem asymptotics.is_O_join

added theorem asymptotics.is_O_mul

added theorem asymptotics.is_O_neg_left

added theorem asymptotics.is_O_neg_right

added theorem asymptotics.is_O_norm_left

added theorem asymptotics.is_O_norm_right

added theorem asymptotics.is_O_of_is_O_const_mul_right

added theorem asymptotics.is_O_refl

added theorem asymptotics.is_O_refl_left

added theorem asymptotics.is_O_smul

added theorem asymptotics.is_O_zero

added theorem asymptotics.is_O_zero_right_iff

deleted theorem asymptotics.is_bigo.add

deleted theorem asymptotics.is_bigo.comp

deleted theorem asymptotics.is_bigo.congr

deleted theorem asymptotics.is_bigo.congr_left

deleted theorem asymptotics.is_bigo.congr_of_sub

deleted theorem asymptotics.is_bigo.congr_right

deleted theorem asymptotics.is_bigo.mono

deleted theorem asymptotics.is_bigo.sub

deleted theorem asymptotics.is_bigo.symm

deleted theorem asymptotics.is_bigo.trans

deleted theorem asymptotics.is_bigo.trans_is_littleo

deleted theorem asymptotics.is_bigo.trans_tendsto

deleted theorem asymptotics.is_bigo.tri

deleted def asymptotics.is_bigo

deleted theorem asymptotics.is_bigo_comm

deleted theorem asymptotics.is_bigo_congr

deleted theorem asymptotics.is_bigo_congr_left

deleted theorem asymptotics.is_bigo_congr_right

deleted theorem asymptotics.is_bigo_const_mul_left

deleted theorem asymptotics.is_bigo_const_mul_left_iff

deleted theorem asymptotics.is_bigo_const_mul_right_iff

deleted theorem asymptotics.is_bigo_const_one

deleted theorem asymptotics.is_bigo_const_smul_left

deleted theorem asymptotics.is_bigo_const_smul_left_iff

deleted theorem asymptotics.is_bigo_const_smul_right

deleted theorem asymptotics.is_bigo_iff

deleted theorem asymptotics.is_bigo_join

deleted theorem asymptotics.is_bigo_mul

deleted theorem asymptotics.is_bigo_neg_left

deleted theorem asymptotics.is_bigo_neg_right

deleted theorem asymptotics.is_bigo_norm_left

deleted theorem asymptotics.is_bigo_norm_right

deleted theorem asymptotics.is_bigo_of_is_bigo_const_mul_right

deleted theorem asymptotics.is_bigo_refl

deleted theorem asymptotics.is_bigo_refl_left

deleted theorem asymptotics.is_bigo_smul

deleted theorem asymptotics.is_bigo_zero

deleted theorem asymptotics.is_bigo_zero_right_iff

deleted theorem asymptotics.is_littleo.add

deleted theorem asymptotics.is_littleo.comp

deleted theorem asymptotics.is_littleo.congr

deleted theorem asymptotics.is_littleo.congr_left

deleted theorem asymptotics.is_littleo.congr_of_sub

deleted theorem asymptotics.is_littleo.congr_right

deleted theorem asymptotics.is_littleo.mono

deleted theorem asymptotics.is_littleo.sub

deleted theorem asymptotics.is_littleo.symm

deleted theorem asymptotics.is_littleo.to_is_bigo

deleted theorem asymptotics.is_littleo.trans

deleted theorem asymptotics.is_littleo.trans_is_bigo

deleted theorem asymptotics.is_littleo.trans_tendsto

deleted theorem asymptotics.is_littleo.tri

deleted def asymptotics.is_littleo

deleted theorem asymptotics.is_littleo_comm

deleted theorem asymptotics.is_littleo_congr

deleted theorem asymptotics.is_littleo_congr_left

deleted theorem asymptotics.is_littleo_congr_right

deleted theorem asymptotics.is_littleo_const_mul_left

deleted theorem asymptotics.is_littleo_const_mul_left_iff

deleted theorem asymptotics.is_littleo_const_mul_right

deleted theorem asymptotics.is_littleo_const_smul_left

deleted theorem asymptotics.is_littleo_const_smul_left_iff

deleted theorem asymptotics.is_littleo_const_smul_right

deleted theorem asymptotics.is_littleo_iff_tendsto

deleted theorem asymptotics.is_littleo_join

deleted theorem asymptotics.is_littleo_mul

deleted theorem asymptotics.is_littleo_mul_left

deleted theorem asymptotics.is_littleo_mul_right

deleted theorem asymptotics.is_littleo_neg_left

deleted theorem asymptotics.is_littleo_neg_right

deleted theorem asymptotics.is_littleo_norm_left

deleted theorem asymptotics.is_littleo_norm_right

deleted theorem asymptotics.is_littleo_of_is_littleo_const_mul_right

deleted theorem asymptotics.is_littleo_one_iff

deleted theorem asymptotics.is_littleo_refl_left

deleted theorem asymptotics.is_littleo_smul

deleted theorem asymptotics.is_littleo_zero

deleted theorem asymptotics.is_littleo_zero_right_iff

added theorem asymptotics.is_o.add

added theorem asymptotics.is_o.comp

added theorem asymptotics.is_o.congr

added theorem asymptotics.is_o.congr_left

added theorem asymptotics.is_o.congr_of_sub

added theorem asymptotics.is_o.congr_right

added theorem asymptotics.is_o.mono

added theorem asymptotics.is_o.sub

added theorem asymptotics.is_o.symm

added theorem asymptotics.is_o.to_is_O

added theorem asymptotics.is_o.trans

added theorem asymptotics.is_o.trans_is_O

added theorem asymptotics.is_o.trans_tendsto

added theorem asymptotics.is_o.tri

added def asymptotics.is_o

added theorem asymptotics.is_o_comm

added theorem asymptotics.is_o_congr

added theorem asymptotics.is_o_congr_left

added theorem asymptotics.is_o_congr_right

added theorem asymptotics.is_o_const_mul_left

added theorem asymptotics.is_o_const_mul_left_iff

added theorem asymptotics.is_o_const_mul_right

added theorem asymptotics.is_o_const_smul_left

added theorem asymptotics.is_o_const_smul_left_iff

added theorem asymptotics.is_o_const_smul_right

added theorem asymptotics.is_o_iff_tendsto

added theorem asymptotics.is_o_join

added theorem asymptotics.is_o_mul

added theorem asymptotics.is_o_mul_left

added theorem asymptotics.is_o_mul_right

added theorem asymptotics.is_o_neg_left

added theorem asymptotics.is_o_neg_right

added theorem asymptotics.is_o_norm_left

added theorem asymptotics.is_o_norm_right

added theorem asymptotics.is_o_of_is_o_const_mul_right

added theorem asymptotics.is_o_one_iff

added theorem asymptotics.is_o_refl_left

added theorem asymptotics.is_o_smul

added theorem asymptotics.is_o_zero

added theorem asymptotics.is_o_zero_right_iff

deleted theorem asymptotics.tendsto_nhds_zero_of_is_littleo

added theorem asymptotics.tendsto_nhds_zero_of_is_o

Modified src/analysis/normed_space/bounded_linear_maps.lean

added theorem is_bounded_linear_map.is_O_comp

added theorem is_bounded_linear_map.is_O_id

added theorem is_bounded_linear_map.is_O_sub

deleted theorem is_bounded_linear_map.is_bigo_comp

deleted theorem is_bounded_linear_map.is_bigo_id

deleted theorem is_bounded_linear_map.is_bigo_sub

Modified src/analysis/normed_space/deriv.lean

deleted theorem has_fderiv_at.is_littleo

added theorem has_fderiv_at.is_o

added theorem has_fderiv_at_filter.is_O_sub

deleted theorem has_fderiv_at_filter.is_bigo_sub

deleted theorem has_fderiv_at_filter.is_littleo

added theorem has_fderiv_at_filter.is_o