linear_inv_isBigO_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem linear_inv_isBigO_left (d : ℤ) {z : ℂ} (hz : z ≠ 0) :
    (fun (c : ℤ) ↦ (c * z + d)⁻¹) =O[cofinite] fun n ↦ (n : ℝ)⁻¹ :=
  (linear_isTheta_left d hz).inv.isBigO

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