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): derivative of a parametric interval integral #10404

Closed
wants to merge 12 commits into from
Closed

[Merged by Bors] - feat(analysis): derivative of a parametric interval integral #10404

wants to merge 12 commits into from

Conversation

urkud
Copy link
Member

@urkud urkud commented Nov 21, 2021 •
edited by github-actions bot

@urkud
feat(measure_theory/integral/interval_integral): add an alternative d…
8fec3c8 
…efinition

Prove that `∫ x in a..b, f x ∂μ = sgn a b • ∫ x in Ι a b, f x ∂μ`,
where `sgn a b = if a ≤ b then 1 else -1`.
@urkud
Apply suggestions from code review
cf3576b
@urkud
feat(analysis/calculus/parametric_integral): generalize, rename
341fec1 
* add `integral` to lemma names;
* a bit more general
  `has_fderiv_at_integral_of_dominated_loc_of_lip'`: only require an
  estimate on `∥F x a - F x₀ a∥` instead of `∥F x a - F y a∥`;
* generalize the `deriv` case to `F : 𝕜 → α → E`, `[is_R_or_C 𝕜]`.
@urkud
Merge branch 'YK-interval-oc' into YK-param-deriv-interval
44e04e5
@urkud
Doc
35ce32b
@urkud
Fix
3e444d2
@urkud
Missing lemma
239e00a
@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. labels Nov 21, 2021
@github-actions github-actions 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 Nov 21, 2021
@github-actions github-actions bot added merge-conflict Please `git merge origin/master` then a bot will remove this label. and removed blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Nov 22, 2021
@github-actions
Copy link

🎉 Great news! Looks like all the dependencies have been resolved:

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

@github-actions github-actions bot removed merge-conflict Please `git merge origin/master` then a bot will remove this label. awaiting-CI The author would like to see what CI has to say before doing more work. labels Nov 23, 2021
@fpvandoorn
Copy link
Member

Have you seen
https://github.com/leanprover-community/sphere-eversion/blob/master/src/parametric_interval_integral.lean ?

If you took this from there, could you also attribute Patrick Massot?

Otherwise, LGTM, but I'll also ask @PatrickMassot to take a look.

@urkud
Copy link
Member Author

urkud commented Nov 23, 2021

Have you seen https://github.com/leanprover-community/sphere-eversion/blob/master/src/parametric_interval_integral.lean ?

No, I haven't. It seems that we should move quite a few lemmas from that file to mathlib.

If you took this from there, could you also attribute Patrick Massot?

Otherwise, LGTM, but I'll also ask @PatrickMassot to take a look.

@fpvandoorn
Copy link
Member

Yes, all of it should go to mathlib (after some cleanup). Do you need the general version (differentiability w.r.t. both a parameter and the integration endpoint at the same time) any time soon?

@urkud
Copy link
Member Author

urkud commented Nov 23, 2021

Do you need the general version (differentiability w.r.t. both a parameter and the integration endpoint at the same time) any time soon?

No.

@PatrickMassot
Copy link
Member

I'm very sorry for the lack of coordination. Of course I should have opened PRs from that file, but I already have a very hard time finding time for the sphere eversion project. I'll try to discuss PR plans with Floris soon. In the mean time we can merge this.
bors merge

@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 Nov 23, 2021
bors bot pushed a commit that referenced this pull request Nov 23, 2021
@urkud
feat(analysis): derivative of a parametric interval integral (#10404)
c192937
@fpvandoorn
Copy link
Member

@PatrickMassot That file is very new, so I wouldn't be too hard on yourself for not PRing it yet. Do you want me to PR everything (except for the C^1 stuff)?

@bors
Copy link

bors bot commented Nov 24, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(analysis): derivative of a parametric interval integral [Merged by Bors] - feat(analysis): derivative of a parametric interval integral Nov 24, 2021
@bors bors bot closed this Nov 24, 2021
@bors bors bot deleted the YK-param-deriv-interval branch November 24, 2021 00:13
ericrbg pushed a commit that referenced this pull request Nov 24, 2021
@urkud @ericrbg
feat(analysis): derivative of a parametric interval integral (#10404)
c7f9938
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@PatrickMassot PatrickMassot Awaiting requested review from PatrickMassot

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
3 participants
@urkud @fpvandoorn @PatrickMassot