[Merged by Bors] - refactor (NumberTheory/ModularForms, Analysis/Complex/UpperHalfPlane) Refactor and clean up coercions by CBirkbeck · Pull Request #18385 · leanprover-community/mathlib4

CBirkbeck · 2024-10-29T13:21:06Z

The code for SL(2, Z) and modular forms had lots of custom local notations, repeated in each file, for certain chains of coercions. We get rid of many of these, and harmonise the remaining ones using scoped (rather than file-local) notations. Separately, we get rid of a lot of annoying duplicate API lemmas by avoiding using subgroups as subtypes unless absolutely necessary.

Co-authored-by: David Loeffler d.loeffler.01@cantab.net

github-actions · 2024-10-29T13:22:15Z

PR summary 0b967b2ef4

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ instCoeFun
+ slash_action_eqn''
++- coe_one
- Gamma0_det
- SlashInvariantFormClass.coe_coe
- mul_slash_subgroup
- subgroupAction
- subgroupGLPos
- subgroupSL
- subgroup_moeb
- subgroup_on_SL_apply
- subgroup_on_glpos
- subgroup_on_glpos_smul_apply
- subgroup_slash
- subgroup_to_SL_tower
- subgroup_to_sl_moeb

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean

loefflerd · 2024-10-30T09:39:54Z

I think we're moving in the right direction here. It's still annoying that we need these up-arrow notations at all, but at least this imposes a bit more order upon them.

I have ~~two~~ ~~three~~ one further refactoring suggestions:

migrate the last 150 lines of LinearAlgebra/Matrix/SpecialLinearGroup.lean (the part which is specific to SL2Z) into Modular.lean, which avoids having two different definitions of the same notation in the same file
~~rename Modular.lean to ModularGroup.lean~~

EDIT: Actually, forget that. The existing Modular file doesn't do what I thought it did, so I'm less convinced this is a good idea; and all this shuffling around is delaying your efforts to add new stuff. I still think we should:

for each scoped notation, say in the docstring for it what namespace it is scoped in (since the mouseover text in VSCode doesn't provide this information automatically)

loefflerd · 2024-10-30T19:14:59Z

!bench

leanprover-bot · 2024-10-30T19:43:02Z

Here are the benchmark results for commit d0fd9f0.
The entire run failed.
Found no significant differences.

loefflerd · 2024-10-30T21:51:29Z

!bench

leanprover-bot · 2024-10-30T22:21:46Z

Here are the benchmark results for commit 0b967b2.
There were significant changes against commit c6c4ad2:

  Benchmark                                         Metric                    Change
  ==================================================================================
+ build                                             .olean serialization       -5.9%
+ build                                             process pre-definitions    -5.1%
+ ~Mathlib.Analysis.Complex.UpperHalfPlane.Basic    instructions              -16.9%
+ ~Mathlib.NumberTheory.ModularForms.SlashActions   instructions              -71.6%

github-actions · 2024-10-30T22:22:10Z

File	Instructions	%
`build`	-639.472⬝10⁹	(-0.47%)
`lint`	-99.924⬝10⁹	(-1.48%)

3 files, Instructions -2.0⬝10⁹

File	Instructions	%
`Mathlib.NumberTheory.ModularForms.CongruenceSubgroups`	-1.123⬝10⁹	(-5.98%)
`Mathlib.NumberTheory.ModularForms.Basic`	-1.339⬝10⁹	(-5.12%)
`Mathlib.NumberTheory.ModularForms.SlashInvariantForms`	-1.812⬝10⁹	(-14.86%)

File	Instructions	%
`Mathlib.NumberTheory.Modular`	-3.264⬝10⁹	(-3.87%)
`Mathlib.Analysis.Complex.UpperHalfPlane.Basic`	-14.453⬝10⁹	(-16.85%)
`Mathlib.NumberTheory.ModularForms.SlashActions`	-58.132⬝10⁹	(-71.60%)

jcommelin

LGTM

bors d=loefflerd

mathlib-bors · 2024-10-31T13:28:08Z

✌️ loefflerd can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

loefflerd · 2024-10-31T13:42:06Z

bors r+

… Refactor and clean up coercions (#18385) The code for SL(2, Z) and modular forms had lots of custom local notations, repeated in each file, for certain chains of coercions. We get rid of many of these, and harmonise the remaining ones using scoped (rather than file-local) notations. Separately, we get rid of a lot of annoying duplicate API lemmas by avoiding using subgroups as subtypes unless absolutely necessary. Co-authored-by: David Loeffler <d.loeffler.01@cantab.net> Co-authored-by: Chris Birkbeck <c.birkbeck@uea.ac.uk> Co-authored-by: Chris Birkbeck <c.birkbeck@ucl.ac.uk>

mathlib-bors · 2024-10-31T13:54:18Z

Pull request successfully merged into master.

Build succeeded:

… Refactor and clean up coercions (#18385) The code for SL(2, Z) and modular forms had lots of custom local notations, repeated in each file, for certain chains of coercions. We get rid of many of these, and harmonise the remaining ones using scoped (rather than file-local) notations. Separately, we get rid of a lot of annoying duplicate API lemmas by avoiding using subgroups as subtypes unless absolutely necessary. Co-authored-by: David Loeffler <d.loeffler.01@cantab.net> Co-authored-by: Chris Birkbeck <c.birkbeck@uea.ac.uk> Co-authored-by: Chris Birkbeck <c.birkbeck@ucl.ac.uk>

CBirkbeck and others added 20 commits October 24, 2024 18:24

Bounds for modular forms of non-positive weights

ab996fc

mk_all

4993ed0

remove @simp

ca095b7

updates

274be6b

golfs

7163c59

name updates

64254fb

renaming and generalising

b12dc3c

fix

decfc00

small golf

565a67d

avoid making subgroups of SL2Z into subtypes

0f3972b

some rev updates

6898da2

scope notation in CongruenceSubgroup namespace

9fa4de7

use MatrixGroup for notation

6f8d112

remove duplicate notations

ba963b7

fix lint

1a1400e

shake imports

3142d7d

lake shake lied to me!

755ab61

fix some ↑ₘₙ notation

e53fb8e

Modular forms small refactor@

b63724a

Modular forms small refactor@

69ce11e

CBirkbeck mentioned this pull request Oct 29, 2024

[Merged by Bors] - feat: bounds for modular forms of non-positive weights #18192

Closed

1 task

doc strings

97d9244

loefflerd reviewed Oct 29, 2024

View reviewed changes

Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean Outdated Show resolved Hide resolved

define notation only once

52171da

loefflerd added 4 commits October 30, 2024 15:05

specify notation scope in docstrings

cb71c91

more de-subtyping of subgroups

01816e3

remove of a whole load of unnecessary ↑ₘ

878be40

remove one coercion notation entirely

250ac08

loefflerd added 3 commits October 30, 2024 19:26

rename

d814998

get rid of yet more coercions

577a3cb

more coercion simplification

d0fd9f0

loefflerd added 4 commits October 30, 2024 21:29

more coercion streamlining

0e8f970

add coercion from GLPos to functions

f194862

Merge remote-tracking branch 'origin/master' into CB_modforms_mm

010db0b

fix merge

0b967b2

loefflerd changed the title ~~Small refactor of Slash invariant forms and Modular forms~~ refactor (NumberTheory/ModularForms, Analysis/Complex/UpperHalfPlane) Refactor and clean up coercions Oct 30, 2024

loefflerd added the t-number-theory Number theory (also use t-algebra or t-analysis to specialize) label Oct 30, 2024

jcommelin reviewed Oct 31, 2024

View reviewed changes

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Oct 31, 2024

mathlib-bors bot changed the title ~~refactor (NumberTheory/ModularForms, Analysis/Complex/UpperHalfPlane) Refactor and clean up coercions~~ [Merged by Bors] - refactor (NumberTheory/ModularForms, Analysis/Complex/UpperHalfPlane) Refactor and clean up coercions Oct 31, 2024

mathlib-bors bot closed this Oct 31, 2024

mathlib-bors bot deleted the CB_modforms_mm branch October 31, 2024 13:54

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - refactor (NumberTheory/ModularForms, Analysis/Complex/UpperHalfPlane) Refactor and clean up coercions#18385

[Merged by Bors] - refactor (NumberTheory/ModularForms, Analysis/Complex/UpperHalfPlane) Refactor and clean up coercions#18385
CBirkbeck wants to merge 33 commits intomasterfrom
CB_modforms_mm

CBirkbeck commented Oct 29, 2024 •

edited by loefflerd

Loading

Uh oh!

github-actions bot commented Oct 29, 2024 •

edited

Loading

Declarations diff

Uh oh!

Uh oh!

loefflerd commented Oct 30, 2024 •

edited

Loading

Uh oh!

loefflerd commented Oct 30, 2024

Uh oh!

leanprover-bot commented Oct 30, 2024

Uh oh!

loefflerd commented Oct 30, 2024

Uh oh!

leanprover-bot commented Oct 30, 2024

Uh oh!

github-actions bot commented Oct 30, 2024

Uh oh!

jcommelin left a comment

Uh oh!

mathlib-bors bot commented Oct 31, 2024

Uh oh!

loefflerd commented Oct 31, 2024

Uh oh!

mathlib-bors bot commented Oct 31, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

CBirkbeck commented Oct 29, 2024 • edited by loefflerd Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Oct 29, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 0b967b2ef4

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

loefflerd commented Oct 30, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

loefflerd commented Oct 30, 2024

Uh oh!

leanprover-bot commented Oct 30, 2024

Uh oh!

loefflerd commented Oct 30, 2024

Uh oh!

leanprover-bot commented Oct 30, 2024

Uh oh!

github-actions bot commented Oct 30, 2024

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Oct 31, 2024

Uh oh!

loefflerd commented Oct 31, 2024

Uh oh!

mathlib-bors bot commented Oct 31, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

CBirkbeck commented Oct 29, 2024 •

edited by loefflerd

Loading

github-actions bot commented Oct 29, 2024 •

edited

Loading

loefflerd commented Oct 30, 2024 •

edited

Loading