Commit 2023-06-28 13:42 5e1c9d6a

View on Github →

feat: port NumberTheory.ModularForms.JacobiTheta.Basic (#5547)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/ModularForms/JacobiTheta/Basic.lean

added theorem continuousAt_jacobiTheta

added theorem differentiableAt_jacobiTheta

added theorem exists_summable_bound_exp_mul_sq

added theorem hasSum_nat_jacobiTheta

added theorem isBigO_at_im_infty_jacobiTheta_sub_one

added theorem jacobiTheta_S_smul

added theorem jacobiTheta_T_sq_smul

added theorem jacobiTheta_eq_tsum_nat

added theorem jacobiTheta_two_add

added theorem norm_exp_mul_sq_le

added theorem norm_jacobiTheta_sub_one_le

added theorem summable_exp_mul_sq