Commit 2023-04-12 19:26 518e4e1e

View on Github →

feat: port Analysis.Asymptotics.Asymptotics (#3393) Because is_O_with, is_O and is_o don't play well with the Lean 4 casing conventions for naming, we have opted for IsBigOWith, IsBigO and IsLittleO in accordance with the Zulip poll

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Asymptotics/Asymptotics.lean

added theorem Asymptotics.IsBigO.add

added theorem Asymptotics.IsBigO.add_isLittleO

added theorem Asymptotics.IsBigO.bound

added theorem Asymptotics.IsBigO.comp_tendsto

added theorem Asymptotics.IsBigO.congr'

added theorem Asymptotics.IsBigO.congr

added theorem Asymptotics.IsBigO.congr_left

added theorem Asymptotics.IsBigO.congr_of_sub

added theorem Asymptotics.IsBigO.congr_right

added theorem Asymptotics.IsBigO.const_mul_left

added theorem Asymptotics.IsBigO.const_mul_right'

added theorem Asymptotics.IsBigO.const_mul_right

added theorem Asymptotics.IsBigO.const_smul_left

added theorem Asymptotics.IsBigO.eq_zero_imp

added theorem Asymptotics.IsBigO.eq_zero_of_norm_pow

added theorem Asymptotics.IsBigO.eq_zero_of_norm_pow_within

added theorem Asymptotics.IsBigO.eventually_mul_div_cancel

added theorem Asymptotics.IsBigO.exists_mem_basis

added theorem Asymptotics.IsBigO.exists_nonneg

added theorem Asymptotics.IsBigO.exists_pos

added theorem Asymptotics.IsBigO.inv_rev

added theorem Asymptotics.IsBigO.isBigOWith

added theorem Asymptotics.IsBigO.isBoundedUnder_le

added theorem Asymptotics.IsBigO.mono

added theorem Asymptotics.IsBigO.mul

added theorem Asymptotics.IsBigO.mul_isLittleO

added theorem Asymptotics.IsBigO.not_isLittleO

added theorem Asymptotics.IsBigO.of_bound'

added theorem Asymptotics.IsBigO.of_bound

added theorem Asymptotics.IsBigO.of_const_mul_right

added theorem Asymptotics.IsBigO.of_pow

added theorem Asymptotics.IsBigO.pow

added theorem Asymptotics.IsBigO.prod_left

added theorem Asymptotics.IsBigO.prod_left_fst

added theorem Asymptotics.IsBigO.prod_left_snd

added theorem Asymptotics.IsBigO.prod_rightl

added theorem Asymptotics.IsBigO.prod_rightr

added theorem Asymptotics.IsBigO.smul

added theorem Asymptotics.IsBigO.smul_isLittleO

added theorem Asymptotics.IsBigO.sub

added theorem Asymptotics.IsBigO.sum

added theorem Asymptotics.IsBigO.sup

added theorem Asymptotics.IsBigO.symm

added theorem Asymptotics.IsBigO.trans

added theorem Asymptotics.IsBigO.trans_eventuallyEq

added theorem Asymptotics.IsBigO.trans_isLittleO

added theorem Asymptotics.IsBigO.trans_le

added theorem Asymptotics.IsBigO.trans_tendsto

added theorem Asymptotics.IsBigO.trans_tendsto_nhds

added theorem Asymptotics.IsBigO.triangle

added theorem Asymptotics.IsBigOWith.add

added theorem Asymptotics.IsBigOWith.add_isLittleO

added theorem Asymptotics.IsBigOWith.comp_tendsto

added theorem Asymptotics.IsBigOWith.congr'

added theorem Asymptotics.IsBigOWith.congr

added theorem Asymptotics.IsBigOWith.congr_const

added theorem Asymptotics.IsBigOWith.congr_left

added theorem Asymptotics.IsBigOWith.congr_right

added theorem Asymptotics.IsBigOWith.const_mul_left

added theorem Asymptotics.IsBigOWith.const_mul_right'

added theorem Asymptotics.IsBigOWith.const_mul_right

added theorem Asymptotics.IsBigOWith.const_smul_left

added theorem Asymptotics.IsBigOWith.eq_zero_imp

added theorem Asymptotics.IsBigOWith.eventually_mul_div_cancel

added theorem Asymptotics.IsBigOWith.exists_eq_mul

added theorem Asymptotics.IsBigOWith.exists_nonneg

added theorem Asymptotics.IsBigOWith.exists_pos

added theorem Asymptotics.IsBigOWith.insert

added theorem Asymptotics.IsBigOWith.inv_rev

added theorem Asymptotics.IsBigOWith.isBigO

added theorem Asymptotics.IsBigOWith.mono

added theorem Asymptotics.IsBigOWith.mul

added theorem Asymptotics.IsBigOWith.of_const_mul_right

added theorem Asymptotics.IsBigOWith.of_pow

added theorem Asymptotics.IsBigOWith.pow'

added theorem Asymptotics.IsBigOWith.pow

added theorem Asymptotics.IsBigOWith.prod_left

added theorem Asymptotics.IsBigOWith.prod_left_fst

added theorem Asymptotics.IsBigOWith.prod_left_same

added theorem Asymptotics.IsBigOWith.prod_left_snd

added theorem Asymptotics.IsBigOWith.prod_rightl

added theorem Asymptotics.IsBigOWith.prod_rightr

added theorem Asymptotics.IsBigOWith.right_le_add_of_lt_1

added theorem Asymptotics.IsBigOWith.right_le_sub_of_lt_1

added theorem Asymptotics.IsBigOWith.smul

added theorem Asymptotics.IsBigOWith.sub

added theorem Asymptotics.IsBigOWith.sub_isLittleO

added theorem Asymptotics.IsBigOWith.sum

added theorem Asymptotics.IsBigOWith.sup'

added theorem Asymptotics.IsBigOWith.sup

added theorem Asymptotics.IsBigOWith.symm

added theorem Asymptotics.IsBigOWith.trans

added theorem Asymptotics.IsBigOWith.trans_isLittleO

added theorem Asymptotics.IsBigOWith.trans_le

added theorem Asymptotics.IsBigOWith.triangle

added theorem Asymptotics.IsBigOWith.weaken

added theorem Asymptotics.IsLittleO.add

added theorem Asymptotics.IsLittleO.add_add

added theorem Asymptotics.IsLittleO.add_isBigO

added theorem Asymptotics.IsLittleO.add_isBigOWith

added theorem Asymptotics.IsLittleO.comp_tendsto

added theorem Asymptotics.IsLittleO.congr'

added theorem Asymptotics.IsLittleO.congr

added theorem Asymptotics.IsLittleO.congr_left

added theorem Asymptotics.IsLittleO.congr_of_sub

added theorem Asymptotics.IsLittleO.congr_right

added theorem Asymptotics.IsLittleO.const_mul_left

added theorem Asymptotics.IsLittleO.const_mul_right'

added theorem Asymptotics.IsLittleO.const_mul_right

added theorem Asymptotics.IsLittleO.const_smul_left

added theorem Asymptotics.IsLittleO.def'

added theorem Asymptotics.IsLittleO.def

added theorem Asymptotics.IsLittleO.eventually_mul_div_cancel

added theorem Asymptotics.IsLittleO.insert

added theorem Asymptotics.IsLittleO.inv_rev

added theorem Asymptotics.IsLittleO.isBigO

added theorem Asymptotics.IsLittleO.isBigOWith

added theorem Asymptotics.IsLittleO.mono

added theorem Asymptotics.IsLittleO.mul

added theorem Asymptotics.IsLittleO.mul_isBigO

added theorem Asymptotics.IsLittleO.not_isBigO

added theorem Asymptotics.IsLittleO.of_const_mul_right

added theorem Asymptotics.IsLittleO.of_pow

added theorem Asymptotics.IsLittleO.pow

added theorem Asymptotics.IsLittleO.prod_left

added theorem Asymptotics.IsLittleO.prod_left_fst

added theorem Asymptotics.IsLittleO.prod_left_snd

added theorem Asymptotics.IsLittleO.prod_rightl

added theorem Asymptotics.IsLittleO.prod_rightr

added theorem Asymptotics.IsLittleO.right_isBigO_add

added theorem Asymptotics.IsLittleO.right_isBigO_sub

added theorem Asymptotics.IsLittleO.smul

added theorem Asymptotics.IsLittleO.smul_isBigO

added theorem Asymptotics.IsLittleO.sub

added theorem Asymptotics.IsLittleO.sum

added theorem Asymptotics.IsLittleO.sup

added theorem Asymptotics.IsLittleO.symm

added theorem Asymptotics.IsLittleO.tendsto_div_nhds_zero

added theorem Asymptotics.IsLittleO.tendsto_inv_smul_nhds_zero

added theorem Asymptotics.IsLittleO.tendsto_zero_of_tendsto

added theorem Asymptotics.IsLittleO.trans

added theorem Asymptotics.IsLittleO.trans_eventuallyEq

added theorem Asymptotics.IsLittleO.trans_isBigO

added theorem Asymptotics.IsLittleO.trans_isBigOWith

added theorem Asymptotics.IsLittleO.trans_le

added theorem Asymptotics.IsLittleO.trans_tendsto

added theorem Asymptotics.IsLittleO.triangle

added theorem Asymptotics.bound_of_isBigO_cofinite

added theorem Asymptotics.bound_of_isBigO_nat_atTop

added theorem Asymptotics.div_isBoundedUnder_of_isBigO

added theorem Asymptotics.isBigOWith_abs_abs

added theorem Asymptotics.isBigOWith_abs_left

added theorem Asymptotics.isBigOWith_abs_right

added theorem Asymptotics.isBigOWith_bot

added theorem Asymptotics.isBigOWith_comm

added theorem Asymptotics.isBigOWith_congr

added theorem Asymptotics.isBigOWith_const_const

added theorem Asymptotics.isBigOWith_const_mul_self

added theorem Asymptotics.isBigOWith_const_one

added theorem Asymptotics.isBigOWith_fst_prod

added theorem Asymptotics.isBigOWith_iff

added theorem Asymptotics.isBigOWith_iff_exists_eq_mul

added theorem Asymptotics.isBigOWith_insert

added theorem Asymptotics.isBigOWith_inv

added theorem Asymptotics.isBigOWith_map

added theorem Asymptotics.isBigOWith_neg_left

added theorem Asymptotics.isBigOWith_neg_right

added theorem Asymptotics.isBigOWith_norm_left

added theorem Asymptotics.isBigOWith_norm_norm

added theorem Asymptotics.isBigOWith_norm_right

added theorem Asymptotics.isBigOWith_of_eq_mul

added theorem Asymptotics.isBigOWith_of_le'

added theorem Asymptotics.isBigOWith_of_le

added theorem Asymptotics.isBigOWith_pi

added theorem Asymptotics.isBigOWith_principal

added theorem Asymptotics.isBigOWith_prod_left

added theorem Asymptotics.isBigOWith_pure

added theorem Asymptotics.isBigOWith_refl

added theorem Asymptotics.isBigOWith_self_const_mul'

added theorem Asymptotics.isBigOWith_self_const_mul

added theorem Asymptotics.isBigOWith_snd_prod

added theorem Asymptotics.isBigOWith_top

added theorem Asymptotics.isBigOWith_zero'

added theorem Asymptotics.isBigOWith_zero

added theorem Asymptotics.isBigOWith_zero_right_iff

added theorem Asymptotics.isBigO_abs_abs

added theorem Asymptotics.isBigO_abs_left

added theorem Asymptotics.isBigO_abs_right

added theorem Asymptotics.isBigO_bot

added theorem Asymptotics.isBigO_cofinite_iff

added theorem Asymptotics.isBigO_comm

added theorem Asymptotics.isBigO_congr

added theorem Asymptotics.isBigO_const_const

added theorem Asymptotics.isBigO_const_const_iff

added theorem Asymptotics.isBigO_const_iff

added theorem Asymptotics.isBigO_const_left_iff_pos_le_norm

added theorem Asymptotics.isBigO_const_mul_left_iff'

added theorem Asymptotics.isBigO_const_mul_left_iff

added theorem Asymptotics.isBigO_const_mul_right_iff'

added theorem Asymptotics.isBigO_const_mul_right_iff

added theorem Asymptotics.isBigO_const_mul_self

added theorem Asymptotics.isBigO_const_of_ne

added theorem Asymptotics.isBigO_const_of_tendsto

added theorem Asymptotics.isBigO_const_one

added theorem Asymptotics.isBigO_const_smul_left

added theorem Asymptotics.isBigO_const_smul_right

added theorem Asymptotics.isBigO_fst_prod'

added theorem Asymptotics.isBigO_fst_prod

added theorem Asymptotics.isBigO_iff

added theorem Asymptotics.isBigO_iff_div_isBoundedUnder

added theorem Asymptotics.isBigO_iff_eventually

added theorem Asymptotics.isBigO_iff_eventually_isBigOWith

added theorem Asymptotics.isBigO_iff_exists_eq_mul

added theorem Asymptotics.isBigO_iff_isBigOWith

added theorem Asymptotics.isBigO_iff_isBoundedUnder_le_div

added theorem Asymptotics.isBigO_map

added theorem Asymptotics.isBigO_nat_atTop_iff

added theorem Asymptotics.isBigO_neg_left

added theorem Asymptotics.isBigO_neg_right

added theorem Asymptotics.isBigO_norm_left

added theorem Asymptotics.isBigO_norm_norm

added theorem Asymptotics.isBigO_norm_right

added theorem Asymptotics.isBigO_of_div_tendsto_nhds

added theorem Asymptotics.isBigO_of_le'

added theorem Asymptotics.isBigO_of_le

added theorem Asymptotics.isBigO_of_subsingleton

added theorem Asymptotics.isBigO_one_iff

added theorem Asymptotics.isBigO_one_nat_atTop_iff

added theorem Asymptotics.isBigO_pi

added theorem Asymptotics.isBigO_principal

added theorem Asymptotics.isBigO_prod_left

added theorem Asymptotics.isBigO_pure

added theorem Asymptotics.isBigO_refl

added theorem Asymptotics.isBigO_refl_left

added theorem Asymptotics.isBigO_self_const_mul'

added theorem Asymptotics.isBigO_self_const_mul

added theorem Asymptotics.isBigO_snd_prod'

added theorem Asymptotics.isBigO_snd_prod

added theorem Asymptotics.isBigO_sup

added theorem Asymptotics.isBigO_top

added theorem Asymptotics.isBigO_zero

added theorem Asymptotics.isBigO_zero_right_iff

added theorem Asymptotics.isLittleO_abs_abs

added theorem Asymptotics.isLittleO_abs_left

added theorem Asymptotics.isLittleO_abs_right

added theorem Asymptotics.isLittleO_bot

added theorem Asymptotics.isLittleO_comm

added theorem Asymptotics.isLittleO_congr

added theorem Asymptotics.isLittleO_const_const_iff

added theorem Asymptotics.isLittleO_const_id_atBot

added theorem Asymptotics.isLittleO_const_id_atTop

added theorem Asymptotics.isLittleO_const_id_comap_norm_atTop

added theorem Asymptotics.isLittleO_const_iff

added theorem Asymptotics.isLittleO_const_iff_isLittleO_one

added theorem Asymptotics.isLittleO_const_left

added theorem Asymptotics.isLittleO_const_left_of_ne

added theorem Asymptotics.isLittleO_const_mul_left_iff'

added theorem Asymptotics.isLittleO_const_mul_left_iff

added theorem Asymptotics.isLittleO_const_mul_right_iff'

added theorem Asymptotics.isLittleO_const_mul_right_iff

added theorem Asymptotics.isLittleO_const_smul_left

added theorem Asymptotics.isLittleO_const_smul_right

added theorem Asymptotics.isLittleO_id_const

added theorem Asymptotics.isLittleO_iff

added theorem Asymptotics.isLittleO_iff_exists_eq_mul

added theorem Asymptotics.isLittleO_iff_forall_isBigOWith

added theorem Asymptotics.isLittleO_iff_nat_mul_le'

added theorem Asymptotics.isLittleO_iff_nat_mul_le

added theorem Asymptotics.isLittleO_iff_nat_mul_le_aux

added theorem Asymptotics.isLittleO_iff_tendsto'

added theorem Asymptotics.isLittleO_iff_tendsto

added theorem Asymptotics.isLittleO_insert

added theorem Asymptotics.isLittleO_irrefl'

added theorem Asymptotics.isLittleO_irrefl

added theorem Asymptotics.isLittleO_map

added theorem Asymptotics.isLittleO_neg_left

added theorem Asymptotics.isLittleO_neg_right

added theorem Asymptotics.isLittleO_norm_left

added theorem Asymptotics.isLittleO_norm_norm

added theorem Asymptotics.isLittleO_norm_pow_id

added theorem Asymptotics.isLittleO_norm_pow_norm_pow

added theorem Asymptotics.isLittleO_norm_right

added theorem Asymptotics.isLittleO_of_subsingleton

added theorem Asymptotics.isLittleO_one_iff

added theorem Asymptotics.isLittleO_one_left_iff

added theorem Asymptotics.isLittleO_pi

added theorem Asymptotics.isLittleO_pow_id

added theorem Asymptotics.isLittleO_pow_pow

added theorem Asymptotics.isLittleO_pow_sub_pow_sub

added theorem Asymptotics.isLittleO_pow_sub_sub

added theorem Asymptotics.isLittleO_prod_left

added theorem Asymptotics.isLittleO_pure

added theorem Asymptotics.isLittleO_refl_left

added theorem Asymptotics.isLittleO_sup

added theorem Asymptotics.isLittleO_top

added theorem Asymptotics.isLittleO_zero

added theorem Asymptotics.isLittleO_zero_right_iff

added theorem Filter.Eventually.isBigO

added theorem Filter.Eventually.trans_isBigO

added theorem Filter.EventuallyEq.trans_isBigO

added theorem Filter.EventuallyEq.trans_isLittleO

added theorem Filter.IsBoundedUnder.isBigO_const

added theorem Filter.Tendsto.isBigO_one

added theorem Homeomorph.isBigOWith_congr

added theorem Homeomorph.isBigO_congr

added theorem Homeomorph.isLittleO_congr

added theorem LocalHomeomorph.isBigOWith_congr

added theorem LocalHomeomorph.isBigO_congr

added theorem LocalHomeomorph.isLittleO_congr

added theorem summable_of_isBigO

added theorem summable_of_isBigO_nat