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 : Filter α) : (fun (x : α) => ↑(f x)) =Θ[l] f

@[simp]

theorem Complex.isLittleO_ofReal_left {α : Type u_1} {E : Type u_2} [Norm E] {l : Filter α} {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 : Filter α} {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 : Filter α} {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 : Filter α} {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 : Filter α} {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 : Filter α} {f : α → E} {g : α → ℝ} : (f =Θ[l] fun (x : α) => ↑(g x)) ↔ f =Θ[l] g