Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-01 10:20 92a5e0b1

View on Github →

feat(analysis/asymptotics): start on bigo and littlo

Estimated changes

Created src/analysis/asymptotics.lean

added theorem asymptotics.is_bigo.add

added theorem asymptotics.is_bigo.comp

added theorem asymptotics.is_bigo.mono

added theorem asymptotics.is_bigo.sub

added def asymptotics.is_bigo

added theorem asymptotics.is_bigo_iff_pos

added theorem asymptotics.is_bigo_mul_left

added theorem asymptotics.is_bigo_mul_right

added theorem asymptotics.is_bigo_neg_left

added theorem asymptotics.is_bigo_neg_right

added theorem asymptotics.is_bigo_norm_left

added theorem asymptotics.is_bigo_norm_right

added theorem asymptotics.is_bigo_of_is_bigo_of_is_bigo

added theorem asymptotics.is_bigo_smul_left

added theorem asymptotics.is_bigo_smul_right

added theorem asymptotics.is_bigo_zero

added theorem asymptotics.is_littleo.add

added theorem asymptotics.is_littleo.comp

added theorem asymptotics.is_littleo.mono

added theorem asymptotics.is_littleo.sub

added theorem asymptotics.is_littleo.to_is_bigo

added def asymptotics.is_littleo

added theorem asymptotics.is_littleo_iff_pos

added theorem asymptotics.is_littleo_iff_tendsto

added theorem asymptotics.is_littleo_mul_left

added theorem asymptotics.is_littleo_mul_right

added theorem asymptotics.is_littleo_neg_left

added theorem asymptotics.is_littleo_neg_right

added theorem asymptotics.is_littleo_norm_left

added theorem asymptotics.is_littleo_norm_right

added theorem asymptotics.is_littleo_of_is_bigo_of_is_littleo

added theorem asymptotics.is_littleo_of_is_littleo_of_is_bigo

added theorem asymptotics.is_littleo_of_tendsto

added theorem asymptotics.is_littleo_smul_left

added theorem asymptotics.is_littleo_smul_right

added theorem asymptotics.is_littleo_zero

added theorem asymptotics.tendsto_nhds_zero_of_is_littleo