# Lemmas about asymptotics and the natural embedding ℝ → ℂ#

In this file we prove several trivial lemmas about Asymptotics.IsBigO etc and (↑) : ℝ → ℂ.

theorem Complex.isTheta_ofReal {α : Type u_1} (f : α) (l : ) :
(fun (x : α) => (f x)) =Θ[l] f
@[simp]
theorem Complex.isLittleO_ofReal_left {α : Type u_1} {E : Type u_2} [Norm E] {l : } {f : α} {g : αE} :
(fun (x : α) => (f x)) =o[l] g f =o[l] g
@[simp]
theorem Complex.isLittleO_ofReal_right {α : Type u_1} {E : Type u_2} [Norm E] {l : } {f : αE} {g : α} :
(f =o[l] fun (x : α) => (g x)) f =o[l] g
@[simp]
theorem Complex.isBigO_ofReal_left {α : Type u_1} {E : Type u_2} [Norm E] {l : } {f : α} {g : αE} :
(fun (x : α) => (f x)) =O[l] g f =O[l] g
@[simp]
theorem Complex.isBigO_ofReal_right {α : Type u_1} {E : Type u_2} [Norm E] {l : } {f : αE} {g : α} :
(f =O[l] fun (x : α) => (g x)) f =O[l] g
@[simp]
theorem Complex.isTheta_ofReal_left {α : Type u_1} {E : Type u_2} [Norm E] {l : } {f : α} {g : αE} :
(fun (x : α) => (f x)) =Θ[l] g f =Θ[l] g
@[simp]
theorem Complex.isTheta_ofReal_right {α : Type u_1} {E : Type u_2} [Norm E] {l : } {f : αE} {g : α} :
(f =Θ[l] fun (x : α) => (g x)) f =Θ[l] g