Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-30 04:06 475f18b6

View on Github →

refactor(analysis/asymptotics): make is_o/is_O work with calc (#14129) Reorder arguments of is_O_with/is_O/is_o as well as trans lemmas so that they work with calc. Also adds f =O[l] g notation. Fixes #2273

Estimated changes

modified theorem asymptotics.is_O.add
modified theorem asymptotics.is_O.add_is_o
modified theorem asymptotics.is_O.bound
modified theorem asymptotics.is_O.congr'
modified theorem asymptotics.is_O.congr
modified theorem asymptotics.is_O.congr_left
modified theorem asymptotics.is_O.exists_pos
modified theorem asymptotics.is_O.inv_rev
modified theorem asymptotics.is_O.is_O_with
modified theorem asymptotics.is_O.join
modified theorem asymptotics.is_O.mono
modified theorem asymptotics.is_O.mul
modified theorem asymptotics.is_O.of_bound
modified theorem asymptotics.is_O.pow
modified theorem asymptotics.is_O.prod_left
modified theorem asymptotics.is_O.smul
modified theorem asymptotics.is_O.smul_is_o
modified theorem asymptotics.is_O.sub
modified theorem asymptotics.is_O.sum
modified theorem asymptotics.is_O.symm
modified theorem asymptotics.is_O.trans
modified theorem asymptotics.is_O.trans_is_o
modified theorem asymptotics.is_O.trans_le
modified theorem asymptotics.is_O.triangle
modified def asymptotics.is_O
modified theorem asymptotics.is_O_bot
modified theorem asymptotics.is_O_comm
modified theorem asymptotics.is_O_congr
modified theorem asymptotics.is_O_const_one
modified theorem asymptotics.is_O_fst_prod'
modified theorem asymptotics.is_O_fst_prod
modified theorem asymptotics.is_O_iff
modified theorem asymptotics.is_O_map
modified theorem asymptotics.is_O_neg_left
modified theorem asymptotics.is_O_neg_right
modified theorem asymptotics.is_O_norm_left
modified theorem asymptotics.is_O_norm_norm
modified theorem asymptotics.is_O_norm_right
modified theorem asymptotics.is_O_of_le'
modified theorem asymptotics.is_O_of_le
modified theorem asymptotics.is_O_principal
modified theorem asymptotics.is_O_prod_left
modified theorem asymptotics.is_O_pure
modified theorem asymptotics.is_O_refl
modified theorem asymptotics.is_O_refl_left
modified theorem asymptotics.is_O_snd_prod'
modified theorem asymptotics.is_O_snd_prod
modified theorem asymptotics.is_O_top
modified theorem asymptotics.is_O_with.add
modified theorem asymptotics.is_O_with.congr
modified theorem asymptotics.is_O_with.is_O
modified theorem asymptotics.is_O_with.join'
modified theorem asymptotics.is_O_with.join
modified theorem asymptotics.is_O_with.mono
modified theorem asymptotics.is_O_with.pow'
modified theorem asymptotics.is_O_with.pow
modified theorem asymptotics.is_O_with.smul
modified theorem asymptotics.is_O_with.sub
modified theorem asymptotics.is_O_with.sum
modified theorem asymptotics.is_O_with.symm
modified theorem asymptotics.is_O_with.trans
modified def asymptotics.is_O_with
modified theorem asymptotics.is_O_with_bot
modified theorem asymptotics.is_O_with_congr
modified theorem asymptotics.is_O_with_iff
modified theorem asymptotics.is_O_with_of_le
modified theorem asymptotics.is_O_with_pure
modified theorem asymptotics.is_O_with_refl
modified theorem asymptotics.is_O_with_top
modified theorem asymptotics.is_O_with_zero'
modified theorem asymptotics.is_O_with_zero
modified theorem asymptotics.is_O_zero
modified theorem asymptotics.is_o.add
modified theorem asymptotics.is_o.add_add
modified theorem asymptotics.is_o.add_is_O
modified theorem asymptotics.is_o.congr'
modified theorem asymptotics.is_o.congr
modified theorem asymptotics.is_o.congr_left
modified theorem asymptotics.is_o.def'
modified theorem asymptotics.is_o.def
modified theorem asymptotics.is_o.inv_rev
modified theorem asymptotics.is_o.is_O
modified theorem asymptotics.is_o.is_O_with
modified theorem asymptotics.is_o.join
modified theorem asymptotics.is_o.mono
modified theorem asymptotics.is_o.mul
modified theorem asymptotics.is_o.mul_is_O
modified theorem asymptotics.is_o.pow
modified theorem asymptotics.is_o.prod_left
modified theorem asymptotics.is_o.smul
modified theorem asymptotics.is_o.smul_is_O
modified theorem asymptotics.is_o.sub
modified theorem asymptotics.is_o.sum
modified theorem asymptotics.is_o.symm
modified theorem asymptotics.is_o.trans
modified theorem asymptotics.is_o.trans_is_O
modified theorem asymptotics.is_o.trans_le
modified theorem asymptotics.is_o.triangle
modified def asymptotics.is_o
modified theorem asymptotics.is_o_bot
modified theorem asymptotics.is_o_comm
modified theorem asymptotics.is_o_congr
modified theorem asymptotics.is_o_iff
modified theorem asymptotics.is_o_map
modified theorem asymptotics.is_o_neg_left
modified theorem asymptotics.is_o_neg_right
modified theorem asymptotics.is_o_norm_left
modified theorem asymptotics.is_o_norm_norm
modified theorem asymptotics.is_o_norm_right
modified theorem asymptotics.is_o_one_iff
modified theorem asymptotics.is_o_prod_left
modified theorem asymptotics.is_o_pure
modified theorem asymptotics.is_o_refl_left
modified theorem asymptotics.is_o_top
modified theorem asymptotics.is_o_zero
modified theorem filter.tendsto.cesaro
modified theorem real.is_o_pow_exp_at_top
deleted theorem real.Gamma_integrand_is_O
modified theorem real.is_o_log_id_at_top
modified theorem real.is_o_pow_log_id_at_top
modified theorem asymptotics.is_O.rpow
modified theorem asymptotics.is_O_with.rpow
modified theorem asymptotics.is_o.rpow
modified theorem is_o_log_rpow_at_top
modified theorem is_o_rpow_exp_at_top
modified theorem roth_number_nat_is_O_id