[Merged by Bors] - Eisenstein series are bounded at infinity by CBirkbeck · Pull Request #12456 · leanprover-community/mathlib4

CBirkbeck · 2024-04-26T18:58:24Z

We show the IsBoundedAtImInfty property for Eisenstein series.

depends on: [Merged by Bors] - feat(Topology/Algebra/InfiniteSum/Order): Add tprod_subtype_le #12600
depends on: [Merged by Bors] - Add(NumberTheory/ModularForms/Identities): periods of modular forms. #12601
depends on: [Merged by Bors] - feat(Analysis/Complex/UpperHalfPlane/Topology): Add lemma #12602
depends on: [Merged by Bors] - Eisenstein series are mdifferentiable #11013
depends on: [Merged by Bors] - Eisenstein series uniform convergence #10377

…mposition.lean Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

…ergence.lean Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

We add a lemma that says the tprod/tsum over a subtype is less than the full sum. Needed for #12456

…12601) Add some basic results about `ModularGroup.T` relating to slash invariant forms of level Gamma(N) and moving elements into verticalStrips. Needed for #12456 Co-authored-by: Chris Birkbeck <c.birkbeck@uea.ac.uk>

Mathlib/NumberTheory/ModularForms/EisensteinSeries/IsBoundedAtImInfty.lean

github-actions · 2024-06-16T21:30:49Z

PR summary 6fb0dc1fb8

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty`	1497

Declarations diff

+ abs_le_tsum_abs
+ eisensteinSeries_SIF_apply
+ isBoundedAtImInfty_eisensteinSeries_SIF
+ summable_norm_eisSummand

You can run this locally as follows

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

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

We add a lemma that says the tprod/tsum over a subtype is less than the full sum. Needed for #12456

…12601) Add some basic results about `ModularGroup.T` relating to slash invariant forms of level Gamma(N) and moving elements into verticalStrips. Needed for #12456 Co-authored-by: Chris Birkbeck <c.birkbeck@uea.ac.uk>

hrmacbeth · 2024-07-02T16:05:56Z

Have you considered using z ^ (-k) rather than 1 / z ^ k in the eisSummand definition? It seems to make the algebra a bit shorter: diff

CBirkbeck · 2024-07-03T08:33:46Z

Have you considered using z ^ (-k) rather than 1 / z ^ k in the eisSummand definition? It seems to make the algebra a bit shorter: diff

Oh I didnt think of that, I didn't know if would this significant a change, but I'm happy with it. ~~Is there an easy way to merge your suggestions into the PR?~~ NVM I think I figured it out.

…unded_at_infty

riccardobrasca

Thanks!

bors d+

Mathlib/NumberTheory/ModularForms/EisensteinSeries/IsBoundedAtImInfty.lean

mathlib-bors · 2024-07-08T07:54:37Z

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

Mathlib/NumberTheory/ModularForms/EisensteinSeries/IsBoundedAtImInfty.lean

CBirkbeck · 2024-07-08T13:05:05Z

bors r+

We show the `IsBoundedAtImInfty` property for Eisenstein series. Co-authored-by: Chris Birkbeck <c.birkbeck@uea.ac.uk> Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>

mathlib-bors · 2024-07-08T13:15:30Z

Pull request successfully merged into master.

Build succeeded:

CBirkbeck and others added 30 commits February 6, 2024 17:48

wip save

1114eea

Update Mathlib/NumberTheory/ModularForms/EisensteinSeries/Finset_Deco…

e9440a2

…mposition.lean Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

Update Mathlib/NumberTheory/ModularForms/EisensteinSeries/Finset_Deco…

e229b84

…mposition.lean Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

Update Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConv…

3a0fc10

…ergence.lean Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

Update Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConv…

b74fe5c

…ergence.lean Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

Update Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConv…

bcf756c

…ergence.lean Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

Update Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConv…

b241e15

…ergence.lean Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

Update Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConv…

a456d5b

…ergence.lean Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

Update Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConv…

eed710a

…ergence.lean Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

Update Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConv…

6b00e1f

…ergence.lean Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

Update Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConv…

0655fb3

…ergence.lean Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

Update Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConv…

b2a5942

…ergence.lean Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

some linting

80e3230

missed one

0b42af4

missed one

8b3ca2e

more lint

3b6159b

more lint

0fc98a5

save

79fe9ac

add file names

a68247d

shake fix

99469cb

save

89c9ee8

sections

8e0f4a8

simplifications, but golfing still needed

3e94fcb

save

6012f67

save2

d63d918

lint fix

bc282a0

golf

49d5d22

save

edf1752

more golf

38ca47f

build fix

b402c36

CBirkbeck added the awaiting-review label May 28, 2024

callesonne pushed a commit that referenced this pull request Jun 4, 2024

feat(Topology/Algebra/InfiniteSum/Order): Add tprod_subtype_le (#12600)

2da2519

We add a lemma that says the tprod/tsum over a subtype is less than the full sum. Needed for #12456

Ruben-VandeVelde reviewed Jun 11, 2024

View reviewed changes

Ruben-VandeVelde added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jun 11, 2024

CBirkbeck added 2 commits June 16, 2024 22:24

rev fixes

6d875a0

merge?

db084b6

CBirkbeck added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jun 16, 2024

js2357 pushed a commit that referenced this pull request Jun 18, 2024

feat(Topology/Algebra/InfiniteSum/Order): Add tprod_subtype_le (#12600)

b2bd384

We add a lemma that says the tprod/tsum over a subtype is less than the full sum. Needed for #12456

use ^ (-k) rather than (^k)^(-1) in eisSummand

436e73b

fix

dcc4c41

Merge remote-tracking branch 'origin/master' into eisensteinSeries_bo…

f5b8be1

…unded_at_infty

CBirkbeck requested a review from riccardobrasca July 7, 2024 17:36

riccardobrasca approved these changes Jul 8, 2024

View reviewed changes

riccardobrasca reviewed Jul 8, 2024

View reviewed changes

Mathlib/NumberTheory/ModularForms/EisensteinSeries/IsBoundedAtImInfty.lean Outdated Show resolved Hide resolved

rev fixes

6fb0dc1

mathlib-bors bot changed the title ~~Eisenstein series are bounded at infinity~~ [Merged by Bors] - Eisenstein series are bounded at infinity Jul 8, 2024

mathlib-bors bot closed this Jul 8, 2024

mathlib-bors bot deleted the eisensteinSeries_bounded_at_infty branch July 8, 2024 13:15

adomani mentioned this pull request Aug 1, 2024

feat: MiM PR report #15355

Open

Conversation

CBirkbeck commented Apr 26, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

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

Uh oh!

PR summary 6fb0dc1fb8

Import changes for modified files

Declarations diff

Uh oh!

hrmacbeth commented Jul 2, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

CBirkbeck commented Jul 3, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

riccardobrasca left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib-bors bot commented Jul 8, 2024

Uh oh!

Uh oh!

CBirkbeck commented Jul 8, 2024

Uh oh!

mathlib-bors bot commented Jul 8, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

CBirkbeck commented Apr 26, 2024 •

edited

Loading

github-actions bot commented Jun 16, 2024 •

edited

Loading

hrmacbeth commented Jul 2, 2024 •

edited

Loading

CBirkbeck commented Jul 3, 2024 •

edited

Loading