Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-26 21:50 a2e8b3c5

View on Github →

feat(special_functions/polynomials): Generalize some polynomial asymptotics to iff statements. (#7545)

Estimated changes

Modified src/analysis/asymptotics/asymptotic_equivalent.lean

added theorem asymptotics.is_equivalent_zero_iff_is_O_zero

Modified src/analysis/special_functions/polynomials.lean

added theorem polynomial.abs_div_tendsto_at_top_of_degree_gt

added theorem polynomial.abs_is_bounded_under_iff

added theorem polynomial.abs_tendsto_at_top_iff

added theorem polynomial.div_tendsto_zero_iff_degree_lt

deleted theorem polynomial.eval_div_tendsto_at_top_of_degree_gt

added theorem polynomial.tendsto_at_bot_iff_leading_coeff_nonpos

added theorem polynomial.tendsto_at_top_iff_leading_coeff_nonneg

added theorem polynomial.tendsto_nhds_iff

Modified src/data/nat/with_bot.lean

added theorem nat.with_bot.one_le_iff_zero_lt

Modified src/order/filter/at_top_bot.lean

added theorem filter.tendsto_const_mul_pow_at_top_iff

added theorem filter.tendsto_neg_const_mul_pow_at_top_iff

Modified src/order/liminf_limsup.lean

added theorem filter.not_is_bounded_under_of_tendsto_at_bot

added theorem filter.not_is_bounded_under_of_tendsto_at_top

Modified src/topology/algebra/ordered/basic.lean

added theorem mul_tendsto_nhds_one_nhds_one

added theorem mul_tendsto_nhds_zero_left

added theorem mul_tendsto_nhds_zero_right

modified theorem nhds_basis_Ioo'

modified theorem nhds_basis_Ioo

added theorem nhds_basis_Ioo_pos

added theorem nhds_basis_Ioo_pos_of_pos

added theorem nhds_basis_abs_sub_lt

added theorem nhds_basis_zero_abs_sub_lt

added theorem nhds_eq_map_mul_left_nhds_one

added theorem nhds_eq_map_mul_right_nhds_one

added theorem tendsto_const_mul_fpow_at_top_zero

added theorem tendsto_const_mul_fpow_at_top_zero_iff

added theorem tendsto_const_mul_pow_nhds_iff

Modified src/topology/separation.lean

added theorem tendsto_const_nhds_iff