Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-01-08 13:16 92841c2e

View on Github →

refactor(analysis/asymptotics): introduce is_O_with (#1857)

  • refactor(analysis/asymptotics): introduce is_O_with I use it to factor out common parts of the proofs of facts about is_O and is_o. It can also be used with principal s filter to operate with ∀ x ∈ s, ∥f x∥ ≤ C * ∥g x∥ is a manner similar to is_O.
  • lint
  • Fix compile
  • Drop (s)mul_same lemmas. It's easy to use (s)mul_is_O (is_O_refl _ _) or (is_O_refl _ _).mul_is_o _ instead
  • docs: say explicitly that is_O is better than is_O_with

Estimated changes

modified theorem asymptotics.is_O.add
deleted theorem asymptotics.is_O.comp
modified theorem asymptotics.is_O.congr
modified theorem asymptotics.is_O.congr_left
added theorem asymptotics.is_O.join
modified theorem asymptotics.is_O.mono
added theorem asymptotics.is_O.mul
added theorem asymptotics.is_O.smul
modified theorem asymptotics.is_O.sub
modified theorem asymptotics.is_O.symm
modified theorem asymptotics.is_O.trans
modified theorem asymptotics.is_O.trans_is_o
deleted theorem asymptotics.is_O.tri
modified def asymptotics.is_O
added theorem asymptotics.is_O_bot
modified theorem asymptotics.is_O_comm
modified theorem asymptotics.is_O_congr
modified theorem asymptotics.is_O_const_one
deleted theorem asymptotics.is_O_iff
deleted theorem asymptotics.is_O_join
deleted theorem asymptotics.is_O_mul
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_right
added theorem asymptotics.is_O_of_le
modified theorem asymptotics.is_O_prod_left
modified theorem asymptotics.is_O_refl
modified theorem asymptotics.is_O_refl_left
deleted theorem asymptotics.is_O_smul
modified theorem asymptotics.is_O_zero
modified theorem asymptotics.is_o.add
deleted theorem asymptotics.is_o.comp
modified theorem asymptotics.is_o.congr
modified theorem asymptotics.is_o.congr_left
added theorem asymptotics.is_o.is_O
added theorem asymptotics.is_o.join
modified theorem asymptotics.is_o.mono
added theorem asymptotics.is_o.mul
added theorem asymptotics.is_o.smul
modified theorem asymptotics.is_o.sub
modified theorem asymptotics.is_o.symm
deleted theorem asymptotics.is_o.to_is_O
modified theorem asymptotics.is_o.trans
modified theorem asymptotics.is_o.trans_is_O
deleted theorem asymptotics.is_o.tri
modified def asymptotics.is_o
added theorem asymptotics.is_o_bot
modified theorem asymptotics.is_o_comm
modified theorem asymptotics.is_o_congr
deleted theorem asymptotics.is_o_join
deleted theorem asymptotics.is_o_mul
deleted theorem asymptotics.is_o_mul_left
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_right
modified theorem asymptotics.is_o_one_iff
modified theorem asymptotics.is_o_prod_left
modified theorem asymptotics.is_o_refl_left
deleted theorem asymptotics.is_o_smul
modified theorem asymptotics.is_o_zero