of_norm_eventuallyLE — Mathlib

English

A simplified variant: if eventually ||f|| ≤ ||g||, then f =O[l] g with c = 1.

Русский

Упрощенный вариант: если неотвлеченно выполняется ||f|| ≤ ||g||, то f =O[l] g с c = 1.

LaTeX

$$IsBigO.of_bound' (h : ∀ᶠ x in l, ‖f x‖ ≤ ‖g x‖) : f =O[l] g$$

Lean4

/-- See also `Filter.Eventually.isBigO`, which is the same lemma
stated using `Filter.Eventually` instead of `Filter.EventuallyLE`. -/
theorem of_norm_eventuallyLE {g : α → ℝ} (h : (‖f ·‖) ≤ᶠ[l] g) : f =O[l] g :=
  .of_bound' <| h.mono fun _ h ↦ h.trans <| le_abs_self _

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