linear_isTheta_right — Mathlib

English

For any integers c and any z ∈ ℂ, the map d ↦ c z + d is Theta relative to the identity on integers along cofinitely many integers.

Русский

Для любого c ∈ ℤ и любого z ∈ ℂ отображение d ↦ c z + d имеет темп роста, равный темпу роста идентичной функции по кофайнсам.

LaTeX

$$$ (d \\mapsto c z + d) =_\\Theta[cofinite] (n \\mapsto n) $$$

Lean4

theorem linear_isTheta_right (c : ℤ) (z : ℂ) : (fun (d : ℤ) ↦ (c * z + d)) =Θ[cofinite] fun n ↦ (n : ℝ) :=
  by
  refine Asymptotics.IsLittleO.add_isTheta ?_ (Int.cast_complex_isTheta_cast_real)
  rw [isLittleO_const_left]
  exact Or.inr (tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding Int.isClosedEmbedding_coe_real)

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