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: improper integration by parts #10874

Closed
wants to merge 9 commits into from
Closed

[Merged by Bors] - feat: improper integration by parts #10874

wants to merge 9 commits into from

Conversation

llllvvuu
Copy link
Collaborator

@llllvvuu llllvvuu commented Feb 23, 2024 •
edited

Open in Gitpod

@llllvvuu llllvvuu force-pushed the feat/integration_by_parts_improper branch 2 times, most recently from 8cbfd70 to 44503e4 Compare February 23, 2024 08:44
@llllvvuu llllvvuu added the WIP Work in progress label Feb 23, 2024
@llllvvuu llllvvuu force-pushed the feat/integration_by_parts_improper branch 2 times, most recently from c130ed0 to 70872f9 Compare February 23, 2024 09:18
@llllvvuu llllvvuu added awaiting-review The author would like community review of the PR awaiting-CI t-analysis Analysis (normed *, calculus) and removed WIP Work in progress labels Feb 23, 2024
@llllvvuu llllvvuu marked this pull request as ready for review February 23, 2024 09:18
@llllvvuu llllvvuu marked this pull request as draft February 23, 2024 09:25
@llllvvuu llllvvuu removed the awaiting-review The author would like community review of the PR label Feb 23, 2024
@llllvvuu llllvvuu marked this pull request as ready for review February 23, 2024 09:28
@llllvvuu llllvvuu added the awaiting-review The author would like community review of the PR label Feb 23, 2024
@llllvvuu llllvvuu force-pushed the feat/integration_by_parts_improper branch from 70872f9 to 449bcba Compare February 23, 2024 09:34
@llllvvuu llllvvuu force-pushed the feat/integration_by_parts_improper branch from 449bcba to 0d40c77 Compare February 23, 2024 09:35
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Feb 27, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Feb 27, 2024
@loefflerd
Copy link
Collaborator

Can you add a section header for the docs? Something like

/-! 
## Integration by parts
-/

It would also be nice to add cross-references in the docstrings between this section and the section in MeasureTheory.Integral.FundThmCalculus with the corresponding results for finite intervals.

@loefflerd loefflerd 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 Mar 6, 2024
@llllvvuu llllvvuu 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 Mar 7, 2024
@llllvvuu
Copy link
Collaborator Author

llllvvuu commented Mar 7, 2024

Added!

@llllvvuu llllvvuu force-pushed the feat/integration_by_parts_improper branch from c5f5c2e to baebc46 Compare March 7, 2024 00:05
@loefflerd
Copy link
Collaborator

Looks good to me!

maintainer merge

@github-actions GitHub Actions
Copy link

github-actions bot commented Mar 7, 2024

🚀 Pull request has been placed on the maintainer queue by loefflerd.

ADedecker
ADedecker approved these changes Mar 7, 2024
View reviewed changes
Copy link
Member

@ADedecker ADedecker left a comment

Choose a reason for hiding this comment

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

Thanks!

bors d+

Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean Outdated Show resolved Hide resolved
Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
(h_zero : Tendsto (u * v) (𝓝[>] a) (𝓝 a')) (h_infty : Tendsto (u * v) atTop (𝓝 b')) :
∫ (x : ℝ) in Ioi a, u' x * v x + u x * v' x = b' - a' := by
rw [← Ici_diff_left] at h_zero
let f := Function.update (u * v) a a'
Copy link
Member

Choose a reason for hiding this comment

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

I would argue that this should instead be handled directly by integral_Ioi_of_hasDerivAt_of_tendsto, which should assume existence of a limit rather than continuity. We could then also avoid changing the function by applying FTC on smaller intervals not touching the left bound. If you want to tinker with it that would be great, otherwise can you leave a TODO/open an issue about it?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I added the TODO comment and started tinkering here https://github.com/leanprover-community/mathlib4/pull/11226/files

@mathlib-bors
Copy link

mathlib-bors bot commented Mar 7, 2024

✌️ llllvvuu 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-mathlib4-bot leanprover-community-mathlib4-bot added delegated and removed awaiting-review The author would like community review of the PR labels Mar 7, 2024
@llllvvuu llllvvuu mentioned this pull request Mar 7, 2024
Draft
1 task
@llllvvuu
Copy link
Collaborator Author

llllvvuu commented Mar 7, 2024

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Mar 7, 2024
@llllvvuu @mo271
feat: improper integration by parts (#10874)
b6e4828 


Co-authored-by: L Lllvvuu <git@llllvvuu.dev>
Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: L <git@llllvvuu.dev>
@mathlib-bors
Copy link

mathlib-bors bot commented Mar 7, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: improper integration by parts [Merged by Bors] - feat: improper integration by parts Mar 7, 2024
@mathlib-bors mathlib-bors bot closed this Mar 7, 2024
@mathlib-bors mathlib-bors bot deleted the feat/integration_by_parts_improper branch March 7, 2024 21:22
kbuzzard pushed a commit that referenced this pull request Mar 12, 2024
@llllvvuu @mo271 @kbuzzard
feat: improper integration by parts (#10874)
0751bb6 


Co-authored-by: L Lllvvuu <git@llllvvuu.dev>
Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: L <git@llllvvuu.dev>
dagurtomas pushed a commit that referenced this pull request Mar 22, 2024
@llllvvuu @mo271 @dagurtomas
feat: improper integration by parts (#10874)
f5db307 


Co-authored-by: L Lllvvuu <git@llllvvuu.dev>
Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: L <git@llllvvuu.dev>
utensil pushed a commit that referenced this pull request Mar 26, 2024
@llllvvuu @mo271 @utensil
feat: improper integration by parts (#10874)
8c956f0 


Co-authored-by: L Lllvvuu <git@llllvvuu.dev>
Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: L <git@llllvvuu.dev>
Louddy pushed a commit that referenced this pull request Apr 15, 2024
@llllvvuu @mo271 @Louddy
feat: improper integration by parts (#10874)
ac62aa2 


Co-authored-by: L Lllvvuu <git@llllvvuu.dev>
Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: L <git@llllvvuu.dev>
callesonne pushed a commit that referenced this pull request Apr 22, 2024
@llllvvuu @mo271 @callesonne
feat: improper integration by parts (#10874)
57f9466 


Co-authored-by: L Lllvvuu <git@llllvvuu.dev>
Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: L <git@llllvvuu.dev>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde left review comments

@ADedecker ADedecker ADedecker approved these changes

Assignees
No one assigned
Labels
delegated maintainer-merge t-analysis Analysis (normed *, calculus)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
6 participants
@llllvvuu @loefflerd @ADedecker @Ruben-VandeVelde @leanprover-community-mathlib4-bot @mo271