Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(analysis/special_functions): Gaussian integral with complex parameter #18090

Closed
wants to merge 13 commits into from
Closed

[Merged by Bors] - feat(analysis/special_functions): Gaussian integral with complex parameter #18090

wants to merge 13 commits into from

Conversation

loefflerd
Copy link
Collaborator

@loefflerd loefflerd commented Jan 7, 2023 •
edited by github-actions bot
Loading

Compute ∫ x:ℝ, exp (-b * x^2) when b is complex (with positive imaginary part).

Open in Gitpod

@mathlib-dependent-issues-bot mathlib-dependent-issues-bot 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 Jan 7, 2023
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot 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 Jan 8, 2023
@mathlib-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

@loefflerd loefflerd marked this pull request as ready for review January 8, 2023 15:22
@loefflerd loefflerd added the awaiting-review The author would like community review of the PR label Jan 8, 2023
sgouezel
sgouezel reviewed Jan 9, 2023
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.

Could you change the file-level docstring to make it up-to-date with the results in the file?

src/analysis/special_functions/gaussian.lean Outdated Show resolved Hide resolved
src/analysis/special_functions/gaussian.lean Outdated Show resolved Hide resolved
src/analysis/special_functions/gaussian.lean Outdated Show resolved Hide resolved
src/analysis/special_functions/gaussian.lean Outdated Show resolved Hide resolved
src/analysis/special_functions/gaussian.lean Outdated Show resolved Hide resolved
src/analysis/special_functions/gaussian.lean Show resolved Hide resolved
@sgouezel sgouezel added awaiting-author A reviewer has asked the author a question or requested changes t-analysis Analysis (normed *, calculus) and removed awaiting-review The author would like community review of the PR labels Jan 9, 2023
@loefflerd loefflerd 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 Jan 11, 2023
sgouezel
sgouezel reviewed Jan 11, 2023
View reviewed changes
src/analysis/special_functions/gaussian.lean Outdated Show resolved Hide resolved
src/analysis/special_functions/gaussian.lean Outdated Show resolved Hide resolved
src/analysis/special_functions/gaussian.lean Outdated Show resolved Hide resolved
src/analysis/special_functions/gaussian.lean Outdated Show resolved Hide resolved
src/topology/connected.lean Outdated Show resolved Hide resolved
src/analysis/special_functions/gaussian.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 Jan 11, 2023
loefflerd and others added 2 commits January 11, 2023 16:47
@loefflerd @sgouezel
Apply suggestions from code review
9f25513 
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
@loefflerd
small syntax fix
055a73b
@loefflerd loefflerd added 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 Jan 11, 2023
@loefflerd
Copy link
Collaborator Author

This is going to take forever to compile all the thousands of intermediate files between topology.connected and special_functions.gaussian, I'll have to wait to make sure I haven't accidentally broken anything in the latter.

@loefflerd loefflerd added awaiting-review The author would like community review of the PR and removed awaiting-CI The author would like to see what CI has to say before doing more work. labels Jan 11, 2023
@loefflerd
Copy link
Collaborator Author

It builds (phew!) 😌

sgouezel
sgouezel reviewed Jan 11, 2023
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.

bors d+
Thanks!

src/analysis/special_functions/gaussian.lean Outdated Show resolved Hide resolved
src/analysis/special_functions/gaussian.lean Outdated Show resolved Hide resolved
@bors
Copy link

bors bot commented Jan 11, 2023

✌️ 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.

@leanprover-community-bot-assistant leanprover-community-bot-assistant added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Jan 11, 2023
@loefflerd
Copy link
Collaborator Author

Thanks for all your help getting these reviewed and merged!

bors r+

bors bot pushed a commit that referenced this pull request Jan 11, 2023
@loefflerd
feat(analysis/special_functions): Gaussian integral with complex para…
0c8d77d 
…meter (#18090)

Compute `∫ x:ℝ, exp (-b * x^2)` when `b` is complex (with positive imaginary part).
@bors
Copy link

bors bot commented Jan 11, 2023

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Jan 11, 2023
@loefflerd
feat(analysis/special_functions): Gaussian integral with complex para…
914cb17 
…meter (#18090)

Compute `∫ x:ℝ, exp (-b * x^2)` when `b` is complex (with positive imaginary part).
@bors
Copy link

bors bot commented Jan 12, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(analysis/special_functions): Gaussian integral with complex parameter [Merged by Bors] - feat(analysis/special_functions): Gaussian integral with complex parameter Jan 12, 2023
@bors bors bot closed this Jan 12, 2023
@bors bors bot deleted the DL_complex_gaussian branch January 12, 2023 00:39
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@sgouezel sgouezel sgouezel left review comments

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions. t-analysis Analysis (normed *, calculus)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@loefflerd @mathlib-dependent-issues-bot @sgouezel @leanprover-community-bot-assistant