English
π|n|^2 |jacobiTheta₂_term(n,z,τ)| ≤ ||jacobiTheta₂_term_fderiv(n,z,τ)||.
Русский
π|n|^2 |jacobiTheta₂_term(n,z,τ)| ≤ ||jacobiTheta₂_term_fderiv(n,z,τ)||.
LaTeX
$$$\pi \cdot |n|^{2} \|\jacobiTheta_2\_term(n,z,\tau)\| \le \|\jacobiTheta_2\_term\_fderiv(n,z,\tau)\|$$$
Lean4
theorem norm_jacobiTheta₂_term_fderiv_ge (n : ℤ) (z τ : ℂ) :
π * |n| ^ 2 * ‖jacobiTheta₂_term n z τ‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖ :=
by
have : ‖(jacobiTheta₂_term_fderiv n z τ) (0, 1)‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖ :=
by
refine (ContinuousLinearMap.le_opNorm _ _).trans ?_
simp_rw [Prod.norm_def, norm_one, norm_zero, max_eq_right zero_le_one, mul_one, le_refl]
refine le_trans ?_ this
simp_rw [jacobiTheta₂_term_fderiv, jacobiTheta₂_term, ContinuousLinearMap.coe_smul', Pi.smul_apply,
ContinuousLinearMap.add_apply, ContinuousLinearMap.coe_smul', ContinuousLinearMap.coe_fst',
ContinuousLinearMap.coe_snd', Pi.smul_apply, smul_zero, zero_add, smul_eq_mul, mul_one, mul_comm _ ‖cexp _‖,
norm_mul]
refine mul_le_mul_of_nonneg_left (le_of_eq ?_) (norm_nonneg _)
simp_rw [norm_real, norm_of_nonneg pi_pos.le, norm_I, mul_one, Int.cast_abs, ← norm_intCast, norm_pow]
