Documentation

Mathlib.Analysis.Asymptotics.Completion

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