English
Let τ be a complex number with positive imaginary part and n an integer. Then the magnitude of exp(π i n^2 τ) is bounded by exp(-π Im τ)^{|n|}. In particular, the bound decays exponentially in |n| as Im(τ) > 0.
Русский
Пусть τ ∈ ℂ с Im(τ) > 0 и n ∈ ℤ. Тогда модуль exp(π i n^2 τ) удовлетворяет неравенству |e^{π i n^2 τ}| ≤ e^{-π Im(τ)}^{|n|}. В частности, этот член ряда экспоненциально убывает при |n| → ∞.
LaTeX
$$$\forall \tau \in \mathbb{C},\ \Im(\tau) > 0,\ \forall n \in \mathbb{Z},\quad \left| e^{\pi i n^{2} \tau} \right| \le \bigl( e^{-\pi \Im(\tau)} \bigr)^{|n|}$$$
Lean4
theorem norm_exp_mul_sq_le {τ : ℂ} (hτ : 0 < τ.im) (n : ℤ) :
‖cexp (π * I * (n : ℂ) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) ^ n.natAbs :=
by
let y := rexp (-π * τ.im)
have h : y < 1 := exp_lt_one_iff.mpr (mul_neg_of_neg_of_pos (neg_lt_zero.mpr pi_pos) hτ)
refine (le_of_eq ?_).trans (?_ : y ^ n ^ 2 ≤ _)
· rw [norm_exp]
have : (π * I * n ^ 2 * τ : ℂ).re = -π * τ.im * (n : ℝ) ^ 2 :=
by
rw [(by push_cast; ring : (π * I * n ^ 2 * τ : ℂ) = (π * n ^ 2 : ℝ) * (τ * I)), re_ofReal_mul, mul_I_re]
ring
obtain ⟨m, hm⟩ := Int.eq_ofNat_of_zero_le (sq_nonneg n)
rw [this, exp_mul, ← Int.cast_pow, rpow_intCast, hm, zpow_natCast]
· have : n ^ 2 = (n.natAbs ^ 2 :) := by rw [Nat.cast_pow, Int.natAbs_sq]
rw [this, zpow_natCast]
exact pow_le_pow_of_le_one (exp_pos _).le h.le ((sq n.natAbs).symm ▸ n.natAbs.le_mul_self)
