English
For S,T>0 and z,τ with |Im z| ≤ S, T ≤ Im τ, one has ‖jacobiTheta₂'_term(n,z,τ)‖ ≤ 2π|n| exp(-π (T n^2 - 2 S |n|)).
Русский
Для S,T>0 и z,τ с |Im z| ≤ S, T ≤ Im τ выполняется ‖jacobiTheta₂'_term(n,z,τ)‖ ≤ 2π|n| exp(-π (T n^2 - 2 S |n|)).
LaTeX
$$$\|\jacobiTheta_2\'_term(n,z,\tau)\| \le 2\pi\,|n|\ e^{ -\pi (T n^{2} - 2 S |n|) }$$$
Lean4
/-- A uniform upper bound for `jacobiTheta₂'_term` on compact subsets. -/
theorem norm_jacobiTheta₂'_term_le {S T : ℝ} (hT : 0 < T) {z τ : ℂ} (hz : |im z| ≤ S) (hτ : T ≤ im τ) (n : ℤ) :
‖jacobiTheta₂'_term n z τ‖ ≤ 2 * π * |n| * rexp (-π * (T * n ^ 2 - 2 * S * |n|)) :=
by
rw [jacobiTheta₂'_term, norm_mul]
refine mul_le_mul (le_of_eq ?_) (norm_jacobiTheta₂_term_le hT hz hτ n) (norm_nonneg _) (by positivity)
simp only [norm_mul, Complex.norm_two, norm_I, Complex.norm_of_nonneg pi_pos.le, norm_intCast, mul_one, Int.cast_abs]
