Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(analysis/complex/phragmen_lindelof): Phragmen-Lindelöf principle for some shapes #13178

Closed
wants to merge 71 commits into from
Closed

[Merged by Bors] - feat(analysis/complex/phragmen_lindelof): Phragmen-Lindelöf principle for some shapes #13178

wants to merge 71 commits into from

Conversation

urkud
Copy link
Member

@urkud urkud commented Apr 5, 2022 •
edited
Loading

urkud added 24 commits March 22, 2022 21:38
@urkud
chore(data/set/intervals): golf, rename
60a8e43 
* rename `set.mem_Ioo_or_eq_endpoints_of_mem_Icc` →
  `set.eq_endpoints_or_mem_Ioo_of_mem_Icc`;
* rename `set.mem_Ioo_or_eq_left_of_mem_Ico` →
  `set.eq_left_or_mem_Ioo_of_mem_Ico`;
* rename `set.mem_Ioo_or_eq_right_of_mem_Ioc` →
  `set.eq_right_or_mem_Ioo_of_mem_Ioc`;
* golf the proofs of these lemmas.

The new names better reflect the order of terms in `or`.
@urkud
Snapshot
5df6929
@urkud
Fix, golf
ec1af87
@urkud
Fix, golf
4eb6100
@urkud
Merge branch 'YK-Icc-golf' into YK-phragmen-lindelof
b5d057a
@urkud
Snapshot
a24fbf1
@urkud
Merge branch 'master' into YK-phragmen-lindelof
3811d90
@urkud
Merge branch 'master' into YK-phragmen-lindelof
59cb2ec
@urkud
Snapshot
00269b2
@urkud
Merge branch 'master' into YK-phragmen-lindelof
a22bd3d
@urkud
Snapshot
69f81bd
@urkud
Merge branch 'master' into YK-phragmen-lindelof
d01150b
@urkud
Merge branch 'master' into YK-phragmen-lindelof
38fc921
@urkud
Snapshot
423829c
@urkud
Merge branch 'master' into YK-phragmen-lindelof
2ede95b
@urkud
Merge branch 'master' into YK-phragmen-lindelof
db7b497
@urkud
Snapshot
8db79df
@urkud
Fix lint
d0a7fe9
@urkud
Fix docs
058f9e9
@urkud
Fix docs
a42f437
@urkud
Merge commit '8db79df776' into YK-phragmen-lindelof
faa0583
@urkud
Merge branch 'YK-diff-cont-on-cl' into YK-phragmen-lindelof
3f591a1
@urkud
Snapshot
221a3e2
@urkud
Revert
b0489e5
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Apr 5, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Apr 9, 2022
@urkud urkud added awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. and removed awaiting-author A reviewer has asked the author a question or requested changes labels May 7, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label May 7, 2022
sgouezel
sgouezel reviewed May 23, 2022
View reviewed changes
Copy link
Collaborator

@sgouezel sgouezel left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have seen a lot of applications of Phragmen-Lindelof in vertical strips. Do you think you could add these versions to this PR? (Otherwise, it can definitely wait for another PR, when it is needed).

src/analysis/complex/phragmen_lindelof.lean Outdated Show resolved Hide resolved
src/analysis/complex/phragmen_lindelof.lean Show resolved Hide resolved
src/analysis/complex/phragmen_lindelof.lean Outdated Show resolved Hide resolved
src/analysis/complex/phragmen_lindelof.lean Outdated Show resolved Hide resolved
src/analysis/complex/phragmen_lindelof.lean Outdated Show resolved Hide resolved
src/analysis/complex/phragmen_lindelof.lean Outdated Show resolved Hide resolved
src/analysis/complex/phragmen_lindelof.lean Outdated Show resolved Hide resolved
src/analysis/complex/phragmen_lindelof.lean Show resolved Hide resolved
src/analysis/complex/phragmen_lindelof.lean Show resolved Hide resolved
src/analysis/complex/phragmen_lindelof.lean Outdated Show resolved Hide resolved
@sgouezel sgouezel added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels May 23, 2022
@urkud urkud changed the title feat(analysis/complex/phragmen_lindelof): Phragmen-Lindelöf principle for a horizontal strip feat(analysis/complex/phragmen_lindelof): Phragmen-Lindelöf principle for some shapes May 27, 2022
@urkud urkud added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels May 27, 2022
@sgouezel
Copy link
Collaborator

bors r+
Thanks!

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels May 27, 2022
bors bot pushed a commit that referenced this pull request May 27, 2022
@urkud
feat(analysis/complex/phragmen_lindelof): Phragmen-Lindelöf principle…
baad002 
… for some shapes (#13178)

Prove Phragmen-Lindelöf principle

- in a horizontal strip;
- in a vertical strip;
- in a coordinate quadrant;
- in the right half-plane (a few versions).
@bors
Copy link

bors bot commented May 27, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(analysis/complex/phragmen_lindelof): Phragmen-Lindelöf principle for some shapes [Merged by Bors] - feat(analysis/complex/phragmen_lindelof): Phragmen-Lindelöf principle for some shapes May 27, 2022
@bors bors bot closed this May 27, 2022
@bors bors bot deleted the YK-phragmen-lindelof branch May 27, 2022 21:20
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@sgouezel sgouezel sgouezel left review comments

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@urkud @mathlib-dependent-issues-bot @sgouezel @semorrison @leanprover-community-bot-assistant