Commit 2020-12-23 12:11 eb5cf252

chore(analysis/asymptotics): a few more lemmas (#5482)

• golf some proofs;
• x ^ n = o (y ^ n) as n → ∞ provided that 0 ≤ x < y;
• lemmas about is_O _ _ ⊤ etc;
• if is_O f g cofinite, then for some C>0 and any x such that g x ≠ 0 we have ∥f x∥≤C*∥g x∥.