isLittleO_ofReal_right — Mathlib

English

Let f: α → E and g: α → ℝ. Viewing g as a complex-valued function via the natural inclusion ℝ ↪ ℂ, we have f = o_l (g · : α → ℂ) if and only if f = o_l g. In other words, the small-o relation is preserved by the real-to-complex embedding.

Русский

Пусть f: α → E и g: α → ℝ. Рассматривая g как функцию в ℂ через единичное вложение ℝ ↪ ℂ, имеем f = o_l (g · : α → ℂ) тогда и только тогда, когда f = o_l g. То есть отношение малого порядка сохраняется под вложением Real в Complex.

LaTeX

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

Lean4

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

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