[Merged by Bors] - feat: interval version of parametric integral lemmas by grunweg · Pull Request #10004 · leanprover-community/mathlib4

grunweg · 2024-01-25T19:27:25Z

Based on code from the sphere eversion project.

depends on: [Merged by Bors] - chore(Calculus/ParametricIntegralInterval): small clean-ups #10005

ghost · 2024-01-26T18:02:44Z

This PR/issue depends on:

~~[Merged by Bors] - chore(Calculus/ParametricIntegralInterval): small clean-ups #10005~~
By Dependent Issues (🤖). Happy coding!

mcdoll

Thank you, I have only a few comments.

mcdoll · 2024-02-11T12:25:41Z

Mathlib/Analysis/Calculus/ParametricIntegral.lean

+    IntervalIntegrable F' μ a b ∧
+      HasFDerivAt (fun x ↦ ∫ t in a..b, F x t ∂μ) (∫ t in a..b, F' t ∂μ) x₀ := by


I would split these into two lemmas.

Sure, I can do this - but since this matches the existing lemmas in this file, I would perform the same split to hasFDerivAt_integral_of_dominated_loc_of_lip and hasFDerivAt_integral_of_dominated_loc_of_lip'.

I just pushed a commit doing so. (Sorry for the force push. Only the last five commits are new.)
I'm out of Lean time for today; I can write docstrings for the new lemmas when I return to this (not before next weekend).

Mathlib/Analysis/Calculus/ParametricIntegral.lean

for differentiating the integral. And fix line lengths from the previous change.

grunweg · 2024-02-11T15:38:42Z

Thank you for the comments; I have addressed them.

grunweg · 2024-02-11T15:48:50Z

@loefflerd One proof in MellinTransform broke, on line 419. I pushed a commit sorry-ing this; I can't fix this quickly.
If you think the commit with the split is a good idea, can you help me fix that proof?

loefflerd · 2024-02-11T15:59:51Z

If you think the commit with the split is a good idea, can you help me fix that proof?

I don't think this split is a good idea.

loefflerd · 2024-02-11T16:09:41Z

The existing lemma bundles stuff together for exactly the same reason that the various hasXXX structures (hasSum, hasDerivAt etc) bundle stuff together – it's pretty much useless to have a formula for deriv f without knowing that f is differentiable, because it might just be a formula for a null value. Likewise, in the case at hand, it's pretty useless to have a lemma "some deriv equals some integral" without knowing that both numbers are actually meaningful.

(IMHO the absence of hasIntegral, bundling together integrability & value of the integral, is a significant shortcoming in the library as it stands.)

loefflerd · 2024-02-11T16:34:38Z

In the interests of debate, I have pushed a commit to this branch showing how the results in MellinTransform can be fixed, if the consensus of the community is that these lemmas should be split. However, I reiterate that I do not support the proposal to split.

grunweg · 2024-02-11T18:53:49Z

@loefflerd Thank you for the prompt fix! Your arguments make sense to me; thank you for elaborating (I certainly learned something).

I personally don't have a horse in this race; I'm happy to implement whatever consensus arises.

loefflerd

Looks good to me!

Ruben-VandeVelde · 2024-02-28T16:54:46Z

Please update the PR summary to reflect the current state of the changes

grunweg · 2024-02-28T18:02:27Z

Sure, done. And merged master, which contained the drive-by syntax changes.

jcommelin

Thanks 🎉

bors merge

Based on code from the sphere eversion project. Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>

mathlib-bors · 2024-03-01T15:31:37Z

Pull request successfully merged into master.

Build succeeded:

Based on code from the sphere eversion project. Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>

grunweg added 6 commits January 25, 2024 18:50

Pull out three hypotheses as variables.

2a7f114

Add a section and pull out two more variables.

e500211

style: use refine (or exact) over refine'

9494f33

style: use \mapsto instead of =>

60eb666

First lemma from sphere-eversion.

1ed86a5

Second lemma.

c6b271b

grunweg added awaiting-review t-analysis Analysis (normed *, calculus) labels Jan 25, 2024

grunweg mentioned this pull request Jan 25, 2024

[Merged by Bors] - chore(Calculus/ParametricIntegralInterval): small clean-ups #10005

Closed

ghost added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Jan 25, 2024

ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 26, 2024

grunweg added 2 commits January 27, 2024 00:36

Merge branch 'master' into MR-sphere-eversion-parametric-integral1

3d1cb78

Fix stray line from merge.

8b55224

ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 26, 2024

mcdoll reviewed Feb 11, 2024

View reviewed changes

grunweg added 6 commits February 11, 2024 15:19

Merge branch 'master' into MR-sphere-eversion-parametric-integral1

75a5adf

Use \centerdot more.

c6b4962

Expand docstrings for the new lemmas.

62b581a

chore: fix Lean 3 syntax in docstrings.

a7ddb2f

chore: use modern syntax for replace

b816b92

Split lemmas in two, one for the integrability hypothesis and another

98da04b

for differentiating the integral. And fix line lengths from the previous change.

grunweg force-pushed the MR-sphere-eversion-parametric-integral1 branch from 55aa142 to 98da04b Compare February 11, 2024 15:37

Narrow down build failure.

8339e51

fix mellin breakage (under protest)

d254c04

jcommelin requested a review from mcdoll February 13, 2024 10:48

ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 18, 2024

grunweg added 2 commits February 18, 2024 21:43

Fully revert the split.

8ab0ca7

Merge branch 'master' into MR-sphere-eversion-parametric-integral1

3763db2

ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 18, 2024

Fix line length.

74390dd

loefflerd approved these changes Feb 27, 2024

View reviewed changes

Merge branch 'master' into MR-sphere-eversion-parametric-integral1

b3adff2

jcommelin approved these changes Mar 1, 2024

View reviewed changes

ghost added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Mar 1, 2024

mathlib-bors bot pushed a commit that referenced this pull request Mar 1, 2024

feat: interval version of parametric integral lemmas (#10004)

9c3a83a

Based on code from the sphere eversion project. Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>

mathlib-bors bot changed the title ~~feat: interval version of parametric integral lemmas~~ [Merged by Bors] - feat: interval version of parametric integral lemmas Mar 1, 2024

mathlib-bors bot closed this Mar 1, 2024

mathlib-bors bot deleted the MR-sphere-eversion-parametric-integral1 branch March 1, 2024 15:31

riccardobrasca pushed a commit that referenced this pull request Mar 1, 2024

feat: interval version of parametric integral lemmas (#10004)

b4df675

Based on code from the sphere eversion project. Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>

kbuzzard pushed a commit that referenced this pull request Mar 12, 2024

feat: interval version of parametric integral lemmas (#10004)

5509299

Based on code from the sphere eversion project. Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>

dagurtomas pushed a commit that referenced this pull request Mar 22, 2024

feat: interval version of parametric integral lemmas (#10004)

9088222

Based on code from the sphere eversion project. Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>

utensil pushed a commit that referenced this pull request Mar 26, 2024

feat: interval version of parametric integral lemmas (#10004)

781da7a

Based on code from the sphere eversion project. Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>

xgenereux pushed a commit that referenced this pull request Apr 15, 2024

feat: interval version of parametric integral lemmas (#10004)

a17a24d

Based on code from the sphere eversion project. Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>

		IntervalIntegrable F' μ a b ∧
		HasFDerivAt (fun x ↦ ∫ t in a..b, F x t ∂μ) (∫ t in a..b, F' t ∂μ) x₀ := by

Conversation

grunweg commented Jan 25, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ghost commented Jan 26, 2024

Uh oh!

mcdoll left a comment

Choose a reason for hiding this comment

Uh oh!

mcdoll Feb 11, 2024

Choose a reason for hiding this comment

Uh oh!

grunweg Feb 11, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

grunweg Feb 11, 2024

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

grunweg commented Feb 11, 2024

Uh oh!

grunweg commented Feb 11, 2024

Uh oh!

loefflerd commented Feb 11, 2024

Uh oh!

loefflerd commented Feb 11, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

loefflerd commented Feb 11, 2024

Uh oh!

grunweg commented Feb 11, 2024

Uh oh!

loefflerd left a comment

Choose a reason for hiding this comment

Uh oh!

Ruben-VandeVelde commented Feb 28, 2024

Uh oh!

grunweg commented Feb 28, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Mar 1, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

grunweg commented Jan 25, 2024 •

edited

Loading

grunweg Feb 11, 2024 •

edited

Loading

loefflerd commented Feb 11, 2024 •

edited

Loading

grunweg commented Feb 28, 2024 •

edited

Loading