Commit 2023-05-18 07:01 c720ca16

View on Github →

chore(number_theory/modular_forms): don't define jacobi_theta on subtype (#19029) In a previous PR, the Jacobi theta function was defined on the subtype ℍ of ℂ and this is slightly annoying to work with. This PR tweaks it to be a function on ℂ (whose values outside ℍ are uninteresting, but well-defined). Split off from #19027.

Estimated changes

Modified src/number_theory/modular_forms/jacobi_theta.lean

added theorem continuous_at_jacobi_theta

deleted theorem continuous_jacobi_theta

added theorem differentiable_at_jacobi_theta

deleted theorem differentiable_at_tsum_exp_mul_sq

modified theorem has_sum_nat_jacobi_theta

modified theorem jacobi_theta_T_sq_smul

modified theorem jacobi_theta_eq_tsum_nat

added theorem jacobi_theta_two_add

deleted theorem jacobi_theta_two_vadd

modified theorem mdifferentiable_jacobi_theta

modified theorem norm_jacobi_theta_sub_one_le