uniform_limit_of_holo_is_holo #13500
Closed
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
CBirkbeck
added
help-wanted
CBirkbeck
added
awaiting-review
|
This PR is quite big... do you think it's possible to split it? Don't worry if at some point you prove preliminary results that are not so interesting without the final one. |
Hmm yeah I thought this might happen, but I didn't have the motivation to do it without being told to :P. I think I can split it up a bit, so I'll do that. |
CBirkbeck
added
awaiting-author
|
Yeah I know... but seeing 735 new lines is scary :) |
bors bot
pushed a commit
that referenced
this pull request
Jun 15, 2022
Also adds various helper lemmas. The purpose of this commit is to provide a computed integral for the `cpow` function. The proof is functionally identical to that of `integral_rpow`, but places a different set of constraints on the various parameters due to different continuity constraints of the cpow function. Some notes on future improvments: * The range of valid integration can be expanded using ae_covers a la #14147 * We currently only contemplate a real argument. However, this should essentially work for any continuous path in the complex plane that avoids the negative real axis. That would require a lot more machinery, not currently in mathlib. Despite these restrictions, why is this important? This, Abel summation, #13500, and #14090 are the key ingredients to bootstrapping Dirichlet series.
bors bot
pushed a commit
that referenced
this pull request
Jun 15, 2022
Also adds various helper lemmas. The purpose of this commit is to provide a computed integral for the `cpow` function. The proof is functionally identical to that of `integral_rpow`, but places a different set of constraints on the various parameters due to different continuity constraints of the cpow function. Some notes on future improvments: * The range of valid integration can be expanded using ae_covers a la #14147 * We currently only contemplate a real argument. However, this should essentially work for any continuous path in the complex plane that avoids the negative real axis. That would require a lot more machinery, not currently in mathlib. Despite these restrictions, why is this important? This, Abel summation, #13500, and #14090 are the key ingredients to bootstrapping Dirichlet series.
bors bot
pushed a commit
that referenced
this pull request
Jul 5, 2022
Some basic definitions and results related to circle integrals of a function. These form part of #13500 Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>
bors bot
pushed a commit
that referenced
this pull request
Jul 5, 2022
Some basic definitions and results related to circle integrals of a function. These form part of #13500 Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>
bors bot
pushed a commit
that referenced
this pull request
Jul 5, 2022
Some basic definitions and results related to circle integrals of a function. These form part of #13500 Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>
bors bot
pushed a commit
that referenced
this pull request
Jul 6, 2022
Some basic definitions and results related to circle integrals of a function. These form part of #13500 Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>
bors bot
pushed a commit
that referenced
this pull request
Jul 7, 2022
Some basic definitions and results related to circle integrals of a function. These form part of #13500 Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>
bors bot
pushed a commit
that referenced
this pull request
Sep 8, 2022
…ives (#14090) This commit proves that the derivative of the pointwise limit of a series of functions is the limit of the derivatives when the derivatives converge uniformly in some closed ball. This and #13500 are two fundamental theorems for bootstrapping the theory of Dirichlet series. This theory underlies my ongoing attempts to prove the density of squarefree integers.
bottine
pushed a commit
that referenced
this pull request
Sep 13, 2022
…ives (#14090) This commit proves that the derivative of the pointwise limit of a series of functions is the limit of the derivatives when the derivatives converge uniformly in some closed ball. This and #13500 are two fundamental theorems for bootstrapping the theory of Dirichlet series. This theory underlies my ongoing attempts to prove the density of squarefree integers.
b-mehta
pushed a commit
that referenced
this pull request
Sep 21, 2022
…ives (#14090) This commit proves that the derivative of the pointwise limit of a series of functions is the limit of the derivatives when the derivatives converge uniformly in some closed ball. This and #13500 are two fundamental theorems for bootstrapping the theory of Dirichlet series. This theory underlies my ongoing attempts to prove the density of squarefree integers.
1 task
|
Replaced by #17074 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Start of file cleanup for the proof that the unifom limit of holomorphic functions is holomorphic.