cexp_neg_quadratic_isLittleO_rpow_atTop

English

Jacobi's theta-function transformation for the sum of exp(-π a n^2 + 2π b n) holds for Re(a) > 0.

Русский

Трансформация функции Джакоби-тета для суммирования exp(-π a n^2 + 2π b n) действует при Re(a) > 0.

LaTeX

$$$$ \\sum_{n\\in \\mathbb{Z}} e^{-\\pi a n^2 + 2\\pi b n} = a^{-1/2}\\, \\sum_{n\\in \\mathbb{Z}} e^{-\\pi/a (n + i b)^2}.$$$$

Lean4

theorem cexp_neg_quadratic_isLittleO_rpow_atTop {a : ℂ} (ha : a.re < 0) (b : ℂ) (s : ℝ) :
    (fun x : ℝ ↦ cexp (a * x ^ 2 + b * x)) =o[atTop] (· ^ s) :=
  by
  apply Asymptotics.IsLittleO.of_norm_left
  convert rexp_neg_quadratic_isLittleO_rpow_atTop ha b.re s with x
  simp_rw [Complex.norm_exp, add_re, ← ofReal_pow, mul_comm (_ : ℂ) ↑(_ : ℝ), re_ofReal_mul, mul_comm _ (re _)]

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