Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-16 17:03 34d37973

View on Github →

feat(number_theory/modular_forms): Jacobi theta function (#18564) Define Jacobi's theta function, and prove its functional equation using Poisson summation.

Estimated changes

Modified src/analysis/complex/upper_half_plane/basic.lean

modified theorem upper_half_plane.modular_S_smul

added theorem upper_half_plane.modular_T_smul

added theorem upper_half_plane.modular_T_zpow_smul

Modified src/analysis/special_functions/gaussian.lean

added theorem complex.tsum_exp_neg_mul_int_sq

modified theorem fourier_transform_gaussian_pi

added theorem is_o_exp_neg_mul_sq_cocompact

added theorem real.tsum_exp_neg_mul_int_sq

added theorem tendsto_rpow_abs_mul_exp_neg_mul_sq_cocompact

Created src/number_theory/modular_forms/jacobi_theta.lean

added theorem jacobi_theta_S_smul

added theorem jacobi_theta_T_sq_smul

added theorem jacobi_theta_summable

added theorem jacobi_theta_two_vadd

added theorem jacobi_theta_unif_summable