English
For all integers n and complex z,τ, the operator norm of jacobiTheta₂_term_fderiv is bounded by 3π|n|^2 times the norm of jacobiTheta₂_term.
Русский
Для всех целых n и комплексных z,τ норма оператора jacobiTheta₂_term_fderiv ограничена 3π|n|^2 умножить на норму jacobiTheta₂_term.
LaTeX
$$$\|\jacobiTheta_2\_term\_fderiv(n,z,\tau)\| \le 3\pi\,|n|^{2}\, \|\jacobiTheta_2\_term(n,z,\tau)\|$$$
Lean4
theorem norm_jacobiTheta₂_term_fderiv_le (n : ℤ) (z τ : ℂ) :
‖jacobiTheta₂_term_fderiv n z τ‖ ≤ 3 * π * |n| ^ 2 * ‖jacobiTheta₂_term n z τ‖ := by
-- this is slow to elaborate so do it once and reuse:
have hns (a : ℂ) (f : (ℂ × ℂ) →L[ℂ] ℂ) : ‖a • f‖ = ‖a‖ * ‖f‖ := norm_smul a f
rw [jacobiTheta₂_term_fderiv, jacobiTheta₂_term, hns, mul_comm _ ‖cexp _‖, (by norm_num : (3 : ℝ) = 2 + 1), add_mul,
add_mul]
refine mul_le_mul_of_nonneg_left ((norm_add_le _ _).trans (add_le_add ?_ ?_)) (norm_nonneg _)
· simp_rw [hns, norm_mul, ← ofReal_ofNat, ← ofReal_intCast, norm_real, norm_of_nonneg zero_le_two,
Real.norm_of_nonneg pi_pos.le, norm_I, mul_one, Real.norm_eq_abs, ← Int.cast_abs, ← Int.cast_pow]
grw [ContinuousLinearMap.norm_fst_le, mul_one, ← Int.le_self_sq]
· simp_rw [hns, norm_mul, one_mul, norm_I, mul_one, norm_real, norm_of_nonneg pi_pos.le, ← ofReal_intCast, ←
ofReal_pow, norm_real, Real.norm_eq_abs, Int.cast_abs, abs_pow]
apply mul_le_of_le_one_right (mul_nonneg pi_pos.le (pow_nonneg (abs_nonneg _) _))
exact ContinuousLinearMap.norm_snd_le ..
