isBigOWith_pi — Mathlib

English

If f1 = o_l f2, then f2 = O_l (f2 − f1).

Русский

Если f1 = o_l f2, тогда f2 = O_l (f2 − f1).

LaTeX

$$$\\displaystyle \\text{If } f_1 = o_l f_2, \\text{ then } f_2 = O_l (f_2 - f_1).$$$

Lean4

theorem isBigOWith_pi {ι : Type*} [Fintype ι] {E' : ι → Type*} [∀ i, NormedAddCommGroup (E' i)] {f : α → ∀ i, E' i}
    {C : ℝ} (hC : 0 ≤ C) : IsBigOWith C l f g' ↔ ∀ i, IsBigOWith C l (fun x => f x i) g' :=
  by
  have : ∀ x, 0 ≤ C * ‖g' x‖ := fun x => mul_nonneg hC (norm_nonneg _)
  simp only [isBigOWith_iff, pi_norm_le_iff_of_nonneg (this _), eventually_all]

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