Mathlib Changelog
v3
Changelog
About
Github
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