English
The norm of jacobiTheta(τ) − 1 decays exponentially as Im(τ) → ∞; more precisely, there is an explicit bound by a multiple of exp(-π Im τ).
Русский
Норма jacobiTheta(τ) − 1 экспоненциально убывает при Im(τ) → ∞; существует явная верхняя граница в виде константы умноженной на exp(-π Im τ).
LaTeX
$$$\|\jacobiTheta\tau - 1\| \le \dfrac{2\, e^{-\pi \Im(\tau)}}{1 - e^{-\pi \Im(\tau)}}$$$
Lean4
/-- An explicit upper bound for `‖jacobiTheta τ - 1‖`. -/
theorem norm_jacobiTheta_sub_one_le {τ : ℂ} (hτ : 0 < im τ) :
‖jacobiTheta τ - 1‖ ≤ 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im) :=
by
suffices ‖∑' n : ℕ, cexp (π * I * ((n : ℂ) + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) / (1 - rexp (-π * τ.im)) by
calc
‖jacobiTheta τ - 1‖ = ↑2 * ‖∑' n : ℕ, cexp (π * I * ((n : ℂ) + 1) ^ 2 * τ)‖ := by
rw [sub_eq_iff_eq_add'.mpr (jacobiTheta_eq_tsum_nat hτ), norm_mul, Complex.norm_two]
_ ≤ 2 * (rexp (-π * τ.im) / (1 - rexp (-π * τ.im))) := by gcongr
_ = 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im) := by rw [div_mul_comm, mul_comm]
have : ∀ n : ℕ, ‖cexp (π * I * ((n : ℂ) + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) ^ (n + 1) :=
by
intro n
simpa only [Int.cast_add, Int.cast_one] using norm_exp_mul_sq_le hτ (n + 1)
have s : HasSum (fun n : ℕ => rexp (-π * τ.im) ^ (n + 1)) (rexp (-π * τ.im) / (1 - rexp (-π * τ.im))) :=
by
simp_rw [pow_succ', div_eq_mul_inv, hasSum_mul_left_iff (Real.exp_ne_zero _)]
exact
hasSum_geometric_of_lt_one (exp_pos (-π * τ.im)).le
(exp_lt_one_iff.mpr <| mul_neg_of_neg_of_pos (neg_lt_zero.mpr pi_pos) hτ)
have aux : Summable fun n : ℕ => ‖cexp (π * I * ((n : ℂ) + 1) ^ 2 * τ)‖ :=
.of_nonneg_of_le (fun n => norm_nonneg _) this s.summable
exact (norm_tsum_le_tsum_norm aux).trans ((aux.tsum_mono s.summable this).trans_eq s.tsum_eq)
