[Merged by Bors] - feat: bounds for modular forms of non-positive weights#18192
[Merged by Bors] - feat: bounds for modular forms of non-positive weights#18192
Conversation
PR summary 7d5154c184Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type |
|---|---|---|
| 1552 | -1 | erw |
Current commit 7d5154c184
Reference commit 66df24a8e2
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
|
Following some discussion with @CBirkbeck, I've pushed some changes to this branch which avoid making subgroups of SL2Z into subtypes, which gets rid of some unnecessary coercions and API lemmas. |
No that was a mistake. I've removed it now and move |
|
(I can push fixes with all these changes to your PR, just let me know if that's OK with you.) |
Oh I was just doing this now. Go ahead and I'll double check there is nothing missing. |
|
I have pushed fixes, I believe everything outside the new file |
CBirkbeck
left a comment
There was a problem hiding this comment.
I think the results like modular_S_smul and those near it should maybe also move down
That doesn't work because it's used in |
loefflerd
left a comment
There was a problem hiding this comment.
Here are some comments on LevelOne.lean.
Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>
Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>
loefflerd
left a comment
There was a problem hiding this comment.
I think this is good now. I just spotted two tiny cosmetic fixes.
maintainer delegate
|
🚀 Pull request has been placed on the maintainer queue by loefflerd. |
|
Thanks! bors d+ |
|
✌️ CBirkbeck can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>
|
bors r+ |
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. Co-authored-by: Chris Birkbeck <c.birkbeck@ucl.ac.uk> Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>
|
Pull request successfully merged into master. Build succeeded: |
add two results:
- If `f` is differentiable on the open unit ball `{z : ℂ | ‖z‖ < 1}`, and `‖f‖` attains a maximum
in this open ball, then `f` is constant
- If `f` is a function differentiable on the open unit ball, and there exists an `r < 1` such that
any value of `‖f‖` on the open ball is bounded above by some value on the closed ball of radius `r`,
then `f` is constant.
These lemmas together with #18192 will be used to prove some dimension results for spaces of modular forms.
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. Co-authored-by: Chris Birkbeck <c.birkbeck@ucl.ac.uk> Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>
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.