Commit 2024-11-20 10:44 ad04df38

View on Github →

feat: bounds for modular forms of non-positive weights (#18192) We use the Maximum modulus principle to show that modular forms of non-positive weights are bounded by its value of some element of the upper half plane imaginary part at least 1/2.

Estimated changes

added def ModularGroup.coe
added theorem ModularGroup.coe_one
added theorem ModularGroup.denom_S
added theorem ModularGroup.det_coe
added theorem ModularGroup.sl_moeb
modified theorem UpperHalfPlane.coe_smul
modified theorem UpperHalfPlane.im_smul
modified theorem UpperHalfPlane.neg_smul
modified theorem UpperHalfPlane.re_smul