isLittleO_const_mul_left_iff — Mathlib

English

If IsBigOWith with c' exists to relate f to c·g, then f = OWith (c'·|c|) relative to g.

Русский

Если существует константа c'≥0 такая, что f = OWith c' l f (c·g), то f = OWith (c'·|c|) l f g.

LaTeX

$$$\text{IsBigOWith}(c', l, f, (\lambda x. c\,g\,x)) \implies \text{IsBigOWith}(c'\cdot \|c\|, l, f, g).$$$

Lean4

theorem isLittleO_const_mul_left_iff {f : α → S} {c : S} (hc : c ≠ 0) : (fun x => c * f x) =o[l] g ↔ f =o[l] g :=
  ⟨(isBigO_self_const_mul hc f l).trans_isLittleO, (isBigO_const_mul_self c f l).trans_isLittleO⟩

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