inv_rev — Mathlib

English

If f = O_l g with a zero-pairing condition (f(x) = 0 implies g(x) = 0 eventually), then g^{-1} = O_l f^{-1}.

Русский

Если f = O_l g и при этом f и g нулевые сопряжены (для больших x, если f(x)=0, тогда g(x)=0), то 1/g = O_l 1/f.

LaTeX

$$$(f : \\alpha\\to\\mathbb{K}) =O_l(g) \\land (\\forall^\\infty x\\in l,\ f(x)=0 \\Rightarrow g(x)=0) \\Rightarrow g(x)^{-1} =O_l f(x)^{-1}.$$$

Lean4

theorem inv_rev {f : α → 𝕜} {g : α → 𝕜'} (h : f =O[l] g) (h₀ : ∀ᶠ x in l, f x = 0 → g x = 0) :
    (fun x => (g x)⁻¹) =O[l] fun x => (f x)⁻¹ :=
  let ⟨_c, hc⟩ := h.isBigOWith
  (hc.inv_rev h₀).isBigO

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