weaken — Mathlib

English

If a scalar-valued function f is Big-O with bound c along a filter l relative to g, then it remains Big-O with any larger bound c' ≥ c along the same l and g.

Русский

Если функция f удовлетворяет условию Big-OWith с константой c вдоль фильтра l относительно g, то она остается Big-OWith для любого большего c' ≥ c вдоль того же l и g.

LaTeX

$$$ IsBigOWith\\ c\\ l\\ f\\ g \\to\\ c \\le c'\\ \\Rightarrow\\ IsBigOWith\\ c'\\ l\\ f\\ g $$$

Lean4

theorem weaken (h : IsBigOWith c l f g') (hc : c ≤ c') : IsBigOWith c' l f g' :=
  IsBigOWith.of_bound <|
    mem_of_superset h.bound fun x hx =>
      calc
        ‖f x‖ ≤ c * ‖g' x‖ := hx
        _ ≤ _ := by gcongr

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