isBigO_const_smul_left — Mathlib

English

IsBigO l f'' (λ _x => c) is equivalent to (c = 0 → f'' =ᶠ[l] 0) ∧ IsBoundedUnder (≤) l (‖f''‖).

Русский

IsBigO l f'' (λ x, c) эквивалентно (c = 0 → f'' ≡ 0 по l) и IsBoundedUnder (≤) l ‖f''‖.

LaTeX

$$$ IsBigO l f'' (\lambda _x. c) \iff (c = 0 \to l\text{-вплоть } f'' = 0) \land IsBoundedUnder (\le) l (\|f''\|). $$$

Lean4

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

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