isBigO_ofReal_left — Mathlib

English

Let f: α → ℝ and g: α → E. Then (f · : α → ℂ) =O[l] g if and only if f =O[l] g; i.e., the Big-O relation is preserved under the real-to-complex embedding.

Русский

Пусть f: α → ℝ и g: α → E. Тогда (f · : α → ℂ) =O[l] g эквивалентно f =O[l] g; то есть отношение Большое-O сохраняется под вложением Real в Complex.

LaTeX

$$$ (f \\cdot : \\alpha \\to \\mathbb{C}) =O[l] g \\leftrightarrow f =O[l] g $$$

Lean4

@[simp, norm_cast]
theorem isBigO_ofReal_left {f : α → ℝ} {g : α → E} : (f · : α → ℂ) =O[l] g ↔ f =O[l] g :=
  (isTheta_ofReal f l).isBigO_congr_left

Похожие утверждения