isBigO_ofReal_right — Mathlib

English

Let f: α → E and g: α → ℝ. Then f =O_l (g · : α → ℂ) iff f =O_l g; i.e., the Big-O relation is preserved when shifting the embedding to the complex side.

Русский

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

LaTeX

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

Lean4

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

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