Commit 2023-03-30 06:36 fe44cd36

View on Github →

feat (number_theory/modular_forms): holomorphy of the Jacobi theta function (#18631) Show that the Jacobi theta function is holomorphic on the upper half-plane, with exponential decay at infinity.

Estimated changes

Modified src/analysis/complex/locally_uniform_limit.lean

added theorem complex.differentiable_on_tsum_of_summable_norm

added theorem complex.has_sum_deriv_of_summable_norm

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

added theorem upper_half_plane.mdifferentiable_coe

added theorem upper_half_plane.smooth_coe

Modified src/number_theory/modular_forms/basic.lean

Modified src/number_theory/modular_forms/jacobi_theta.lean

added theorem continuous_jacobi_theta

added theorem differentiable_at_tsum_exp_mul_sq

added theorem exists_summable_bound_exp_mul_sq

added theorem has_sum_nat_jacobi_theta

added theorem is_O_at_im_infty_jacobi_theta_sub_one

added theorem jacobi_theta_eq_tsum_nat

deleted theorem jacobi_theta_summable

deleted theorem jacobi_theta_unif_summable

added theorem mdifferentiable_jacobi_theta

added theorem norm_exp_mul_sq_le

added theorem norm_jacobi_theta_sub_one_le

added theorem summable_exp_mul_sq