isTheta_const_smul_left — Mathlib

English

A variant of const-scalar-left Theta equivalence with a simplified scalar action, under nonzero scalar.

Русский

Вариант эквивалентности Θ слева от константы, при ненулевом скалярном множителе.

LaTeX

$$$ c \neq 0 \Rightarrow (\;f' =Θ_l (c·g')\; \Leftrightarrow\; (f' =Θ_l g') ) $.$$

Lean4

theorem isTheta_const_smul_left [NormedSpace 𝕜 E'] {c : 𝕜} (hc : c ≠ 0) : (fun x ↦ c • f' x) =Θ[l] g ↔ f' =Θ[l] g :=
  and_congr (isBigO_const_smul_left hc) (isBigO_const_smul_right hc)

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