Commit 2024-01-17 14:32 2366dbdf

View on Github →

feat(NumberTheory/ModularForms): two-variable Jacobi theta (#9666) Add a more general version of the Jacobi theta function with a second variable, and prove the transformation law for this more general function rather than just for the one-variable version. Preparatory to functional equations for Dirichlet L-functions.

Estimated changes

added theorem Complex.I_pow_four
modified theorem continuousAt_jacobiTheta
modified theorem hasSum_nat_jacobiTheta
modified theorem jacobiTheta_eq_tsum_nat
modified theorem jacobiTheta_two_add
modified theorem norm_exp_mul_sq_le
modified theorem norm_jacobiTheta_sub_one_le
modified theorem summable_exp_mul_sq