theorem Asymptotics.isLittleO_const_id_cocompact {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] [ProperSpace F''] (c : E'') : (fun (_x : F'') => c) =o[Filter.cocompact F''] id

theorem Asymptotics.isLittleO_const_id_atTop2 {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] [LinearOrder F''] [NoMaxOrder F''] [ClosedIciTopology F''] [ProperSpace F''] (c : E'') : (fun (_x : F'') => c) =o[Filter.atTop] id

theorem Asymptotics.isLittleO_const_id_atBot2 {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] [LinearOrder F''] [NoMinOrder F''] [ClosedIicTopology F''] [ProperSpace F''] (c : E'') : (fun (_x : F'') => c) =o[Filter.atBot] id

theorem Filter.Eventually.natCast {f : ℝ → Prop} (hf : ∀ᶠ (x : ℝ) in atTop, f x) : ∀ᶠ (n : ℕ) in atTop, f ↑n

theorem Asymptotics.IsBigO.natCast {E : Type u_3} [Norm E] {f g : ℝ → E} (h : f =O[Filter.atTop] g) : (fun (n : ℕ) => f ↑n) =O[Filter.atTop] fun (n : ℕ) => g ↑n