Asymptotics in the completion of a normed space

In this file we prove lemmas relating f = O(g) etc for composition of functions with coercion of a seminormed group to its completion.

@[simp]

theorem Asymptotics.isBigO_completion_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [Norm E] [SeminormedAddCommGroup F] {f : α → E} {g : α → F} {l : Filter α} : (fun (x : α) => ↑(g x)) =O[l] f ↔ g =O[l] f

@[simp]

theorem Asymptotics.isBigO_completion_right {α : Type u_1} {E : Type u_2} {F : Type u_3} [Norm E] [SeminormedAddCommGroup F] {f : α → E} {g : α → F} {l : Filter α} : (f =O[l] fun (x : α) => ↑(g x)) ↔ f =O[l] g

@[simp]

theorem Asymptotics.isTheta_completion_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [Norm E] [SeminormedAddCommGroup F] {f : α → E} {g : α → F} {l : Filter α} : (fun (x : α) => ↑(g x)) =Θ[l] f ↔ g =Θ[l] f

@[simp]

theorem Asymptotics.isTheta_completion_right {α : Type u_1} {E : Type u_2} {F : Type u_3} [Norm E] [SeminormedAddCommGroup F] {f : α → E} {g : α → F} {l : Filter α} : (f =Θ[l] fun (x : α) => ↑(g x)) ↔ f =Θ[l] g

@[simp]

theorem Asymptotics.isLittleO_completion_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [Norm E] [SeminormedAddCommGroup F] {f : α → E} {g : α → F} {l : Filter α} : (fun (x : α) => ↑(g x)) =o[l] f ↔ g =o[l] f

@[simp]

theorem Asymptotics.isLittleO_completion_right {α : Type u_1} {E : Type u_2} {F : Type u_3} [Norm E] [SeminormedAddCommGroup F] {f : α → E} {g : α → F} {l : Filter α} : (f =o[l] fun (x : α) => ↑(g x)) ↔ f =o[l] g