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

theorem Complex.isBigO_comp_ofReal_nhds {f g : ℂ → ℂ} {x : ℝ} (h : f =O[nhds ↑x] g) : (fun (y : ℝ) => f ↑y) =O[nhds x] fun (y : ℝ) => g ↑y

theorem Complex.isBigO_comp_ofReal_nhds_ne {f g : ℂ → ℂ} {x : ℝ} (h : f =O[nhdsWithin ↑x {↑x}ᶜ] g) : (fun (y : ℝ) => f ↑y) =O[nhdsWithin x {x}ᶜ] fun (y : ℝ) => g ↑y

theorem Complex.isBigO_re_sub_re {z : ℂ} : (fun (w : ℂ) => w.re - z.re) =O[nhds z] fun (w : ℂ) => w - z

theorem Complex.isBigO_im_sub_im {z : ℂ} : (fun (w : ℂ) => w.im - z.im) =O[nhds z] fun (w : ℂ) => w - z

theorem Int.cast_complex_isTheta_cast_real : Int.cast =Θ[Filter.cofinite] Int.cast