Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-18 16:59 4264220c

View on Github →

feat(analysis/asymptotics): add several lemmas (#14805) Also make 𝕜 explicit in asymptotics.is_O_with_const_one and asymptotics.is_O_const_one.

Estimated changes

Modified src/analysis/asymptotics/asymptotic_equivalent.lean

added theorem asymptotics.is_o.add_is_equivalent

Modified src/analysis/asymptotics/asymptotics.lean

Modified src/analysis/asymptotics/theta.lean

added theorem asymptotics.is_Theta.div

added theorem asymptotics.is_Theta.trans_eventually_eq

added theorem asymptotics.is_Theta_norm_left

added theorem asymptotics.is_Theta_norm_right

added theorem asymptotics.is_Theta_of_norm_eventually_eq'

added theorem asymptotics.is_Theta_of_norm_eventually_eq

modified theorem asymptotics.is_Theta_refl

added theorem asymptotics.is_Theta_rfl

added theorem filter.eventually_eq.trans_is_Theta