linear_inv_isBigO_right — Mathlib

English

For c ∈ ℤ and z ∈ ℂ, the inverse map d ↦ (c z + d)^{-1} is Big-O of n^{-1} along cofinitely many integers.

Русский

Для c ∈ ℤ и z ∈ ℂ обратная функция d ↦ (c z + d)^{-1} есть в общем смысле Big-O по n^{-1} вдоль cofinitely многих целых.

LaTeX

$$$ (d \\mapsto (c z + d)^{-1}) = O_{cofinite} (n \\mapsto n^{-1}) $$$

Lean4

theorem linear_inv_isBigO_right (c : ℤ) (z : ℂ) : (fun (d : ℤ) ↦ (c * z + d)⁻¹) =O[cofinite] fun n ↦ (n : ℝ)⁻¹ :=
  (linear_isTheta_right c z).inv.isBigO

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