linear_isTheta_left — Mathlib

English

For any integer d and any nonzero z ∈ ℂ, the map c ↦ c z + d is Theta(cofinite) to n.

Русский

Для любого целого d и любого не нулевого z ∈ ℂ отображение c ↦ c z + d имеет темп роста Theta(cofinite) по отношению к n.

LaTeX

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

Lean4

theorem linear_isTheta_left (d : ℤ) {z : ℂ} (hz : z ≠ 0) : (fun (c : ℤ) ↦ (c * z + d)) =Θ[cofinite] fun n ↦ (n : ℝ) :=
  by
  apply IsTheta.add_isLittleO
  · simp_rw [mul_comm]
    apply Asymptotics.IsTheta.const_mul_left hz Int.cast_complex_isTheta_cast_real
  ·
    simp only [isLittleO_const_left, Int.cast_eq_zero,
      tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding Int.isClosedEmbedding_coe_real, or_true]

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