isBigO_const_smul_right — Mathlib

English

If f = O_l (λ x => c • f' x) and g = λ x => c • f' x with c ≠ 0, then f = O_l f'.

Русский

Если f = O_l (λ x, c • f'(x)) и c ≠ 0, то f = O_l f'.

LaTeX

$$$ (f =O[l] (\lambda x => c • f' x)) \land (c \neq 0) \Rightarrow f =O[l] f'. $$$

Lean4

theorem isBigO_const_smul_right {c : 𝕜} (hc : c ≠ 0) : (f =O[l] fun x => c • f' x) ↔ f =O[l] f' :=
  by
  have cne0 : ‖c‖ ≠ 0 := norm_ne_zero_iff.mpr hc
  rw [← isBigO_norm_right]
  simp only [norm_smul]
  rw [isBigO_const_mul_right_iff cne0, isBigO_norm_right]

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