[Merged by Bors] - feat(analysis/convolution): regularity of convolution for functions depending on a parameter #17626

sgouezel · 2022-11-19T18:35:05Z

Show that the convolution of f and g is smooth when g is. A version of this statement is already in mathlib, but in this PR we prove the version where g depends on a parameter.

depends on: [Merged by Bors] - feat(measure_theory/integral/bochner): continuity statements within a set for integrals #17625

mathlib-dependent-issues-bot · 2022-12-02T20:34:48Z

This PR/issue depends on:

~~[Merged by Bors] - feat(measure_theory/integral/bochner): continuity statements within a set for integrals #17625~~
By Dependent Issues (🤖). Happy coding!

fpvandoorn · 2022-12-14T18:49:52Z

I have some big comments, but we can definitely merge this before you've addressed all the comments, in order to not delay the bump function refactor. But maybe you can give a stab at some of them.

It would be nice to follow the continuity lemma statement note: https://leanprover-community.github.io/mathlib_docs/notes.html#continuity%20lemma%20statement
I already went ahead and modified the continuous_on lemma using that, and the proof became easier.
I guess that it makes the fderiv lemma statement more complicated and for the cont_diff the induction works better without it, so maybe it's not too relevant for the other ones (but it might be nice to prove versions that follow the continuity lemma statement afterwards)
It would be nice to prove the non-parametric versions from these. For the continuity lemma you have much stronger type-class assumptions (the non-parametric version works for locally compact groups that might not be abelian), so that would require changing the proof to simpler type classes. For cont_diff do you have stronger type-class assumptions? If not, it would be nice to derive the old version from it (which is trivial if you have a version that follows the aforementioned library note).
I noticed that you went for the induction proof where you have to deal with universe levels instead of the proof where you use cont_diff_succ_iff_fderiv_apply. Is the problem that to use cont_diff_succ_iff_fderiv_apply you need that P is finite dimensional, which you do not assume?
I dislike these 100+ line proofs, since I find them hard to maintain, and they have the tendency to reprove small lemmas multiple times that could be factored out. For example, can you separate out a lemma like a parametric version of has_compact_support.convolution_integrand_bound_right which you can then maybe use both in the continuity and differentiability proof (has_compact_support.convolution_integrand_bound_right is used in both the continuity and differentiability proof in the non-parametric case)?

sgouezel · 2022-12-15T08:04:58Z

I noticed that you went for the induction proof where you have to deal with universe levels instead of the proof where you use cont_diff_succ_iff_fderiv_apply. Is the problem that to use cont_diff_succ_iff_fderiv_apply you need that P is finite dimensional, which you do not assume?

Yes, that's exactly the issue: P being finite-dimensional is not relevant for the statement, but the proof with cont_diff_succ_iff_fderiv_apply would need it.

fpvandoorn · 2022-12-15T11:45:45Z

It's really unfortunate that we need to do deal with these universe issues if we want to do a cont_diff induction proof in full generality...

sgouezel · 2022-12-22T14:46:02Z

Here are the changes I've made:

I have given versions of the continuity and smoothness statements following the library note (but I have also kept the original versions as they can be handy)
I have deduced the smoothness statement without parameters from the version with parameters

Changes I haven't made:

The assumptions for continuity with/without parameters are currently orthogonal (one requires local compactness, the other one requires vector space but no local compactness). I can get a version covering the two, but for this I need to refactor the definition of locally_integrable (which currently only makes sense on locally compact spaces -- instead of requiring finite integrals on compact sets one should require finite integral on a neighborhood of each point, just like is_locally_finite_measure is defined).
I haven't cut the proofs into shorter lemmas, as once the locally_integrable refactor is done the proofs should become much easier to streamline.

I'd rather keep the refactor for another PR, so for me this looks good to go.

sgouezel · 2022-12-25T15:33:56Z

I refactor locally_integrable in #18012. There is no direct dependence between this PR and the other. Whichever is merged first, I will adapt the other one.

fpvandoorn

LGTM

bors d+
You can choose the order in which you want to merge the two PRs. If unifying the two PRs is nontrivial, I'm happy to quickly review the unification too.

fpvandoorn · 2023-01-04T16:33:43Z

src/analysis/convolution.lean

+  {g : P → G → E'} {s : set P} (h'u : maps_to u a s) {k : set G}
+  (hk : is_compact k) (hgs : ∀ p, ∀ x, p ∈ s → x ∉ k → g p x = 0)
+  (hf : locally_integrable f μ) (hg : continuous_on (↿g) (s ×ˢ univ)) :
+  continuous_on (λ x, (f ⋆[L, μ] g (u x)) (v x)) a :=


I think you can remove u, and just write f ⋆[L, μ] g x in the conclusion.
If I then want to prove continuous_on (λ x, (f ⋆[L, μ] g' (u x)) (v x)) a in an application, I can just set g x y := g' (u x) y.
Removing u will also make it a lot easier for the elaborator to unify this lemma with an application, without giving g or u explicitly (or via other arguments).
EDIT: Same below. Also, without the u you don't have to cook up an arbitrary u in has_compact_support.cont_diff_convolution_right

I am doubtful about that: if I have a lemma on continuity and I need to apply it to a composition, the library note you wrote suggests precisely to have a lemma that generalizes over all parameters because it is much more flexible in this way. It would feel awkward to generalize one variable but not the other one...

For instance, in my application below, if I just use g x, then since the parameter space is just unit it means that I will have to take x : unit and I can't deduce anything out of it. On the other hand, with g (u x), I can use as u any constant map into unit, and in particular I can take x : G, which is what I need.

g is the parameter, and you generalize it by making it a binary function and replacing it with g x.
In your application below, g_{this lemma} x y := g_{lemma below} y, and there is no issue, and you don't have to cook up a random u yourself. EDIT: in particular the parameter space is not unit under my approach, there is no unit in sight of either lemma.

To be more precise about parameters, here is the way I think about it. We are working with the function
(g, v) \mapsto (f ⋆[L, μ] g) v (we could also make the function depend on f or L, but we're not doing this in the current lemma). If we want to make the most general continuity/differentiability lemma, we are interested in making both g and v depend on a new variable x, so making g a binary function and v a unary function (it was a nullary function before) and then we are considering the map x \mapsto (f ⋆[L, μ] g x) (v x).
You don't want g (u x) for the same reason you don't want (v (u x)).

Thanks for the clarification. I'm convinced!

bors · 2023-01-04T16:40:09Z

✌️ sgouezel can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

fpvandoorn · 2023-01-06T11:10:39Z

Thanks!

bors merge

…epending on a parameter (#17626) Show that the convolution of `f` and `g` is smooth when `g` is. A version of this statement is already in mathlib, but in this PR we prove the version where `g` depends on a parameter. Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>

sgouezel · 2023-01-06T13:06:30Z

bors r-
Sorry, still working on it

bors · 2023-01-06T13:06:32Z

Canceled.

fpvandoorn · 2023-01-06T14:13:23Z

Oh, my bad!

sgouezel · 2023-01-07T07:53:28Z

I'm done with the cleanup. The new changes:

obtain a general version for continuity of convolution with parameters (no commutativity or normed group assumption). Deduce the continuity without parameters from it.
Streamline the proof of the formula for the derivative of convolution with parameters, by using existing lemmas instead of ad hoc arguments in the proof, and don't separate any more in the proof the finite/infinite dimensional cases. This shortens the proof by 50 lines (but it's still long!)

I know it's already delegated, but since the changes are macroscopic, you may want to have a look (or trust me on this one!), so I'm marking this as awaiting-review again.

fpvandoorn · 2023-01-07T13:23:27Z

This looks a lot better, and thanks for giving me another look after these major changes.

bors merge

…epending on a parameter (#17626) Show that the convolution of `f` and `g` is smooth when `g` is. A version of this statement is already in mathlib, but in this PR we prove the version where `g` depends on a parameter. Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>

bors · 2023-01-07T15:56:12Z

Pull request successfully merged into master.

Build succeeded:

sgouezel added 5 commits November 18, 2022 13:04

cherry pick

b84c2c9

start on removing openness assumption

d06e32f

relativize bounds

e895060

relativize

86a2e29

remove openness assumption

a221163

sgouezel requested a review from a team as a code owner November 19, 2022 18:35

sgouezel mentioned this pull request Nov 19, 2022

[Merged by Bors] - feat(analysis/calculus/special_functions): refactor bump functions #17453

Closed

10 tasks

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 Nov 19, 2022

lint

9b1aeaa

sgouezel added awaiting-review The author would like community review of the PR t-analysis Analysis (normed *, calculus) labels Nov 20, 2022

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 Dec 2, 2022

sgouezel added 4 commits December 3, 2022 08:43

merge upstream

65ff738

cleanup

ab49a6c

cleanup

eda2656

cleanup

665ea6d

sgouezel requested a review from fpvandoorn December 4, 2022 09:37

checkpoint

8c9283b

fpvandoorn 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 Dec 15, 2022

cleanup

5b91eac

sgouezel 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 Dec 22, 2022

sgouezel mentioned this pull request Dec 25, 2022

[Merged by Bors] - feat(analysis/convolution): weaken topological assumptions #18012

Closed

fpvandoorn reviewed Jan 4, 2023

View reviewed changes

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 4, 2023

sgouezel added 3 commits January 5, 2023 18:21

merge master

5094683

fix merge

390be36

remove u

b129a36

github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Jan 6, 2023

sgouezel added 4 commits January 6, 2023 17:37

start streamlining

bebed94

fix

be5871f

cleanup

4de35cb

lint

0167b96

sgouezel added awaiting-review The author would like community review of the PR and removed ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) delegated The PR author may merge after reviewing final suggestions. labels Jan 7, 2023

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 Jan 7, 2023

bors bot changed the title ~~feat(analysis/convolution): regularity of convolution for functions depending on a parameter~~ [Merged by Bors] - feat(analysis/convolution): regularity of convolution for functions depending on a parameter Jan 7, 2023

bors bot closed this Jan 7, 2023

bors bot deleted the convol_with_params branch January 7, 2023 15:56

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(analysis/convolution): regularity of convolution for functions depending on a parameter #17626

[Merged by Bors] - feat(analysis/convolution): regularity of convolution for functions depending on a parameter #17626

sgouezel commented Nov 19, 2022 •

edited by github-actions bot

mathlib-dependent-issues-bot commented Dec 2, 2022

fpvandoorn commented Dec 14, 2022

sgouezel commented Dec 15, 2022 •

edited by alreadydone

fpvandoorn commented Dec 15, 2022

sgouezel commented Dec 22, 2022 •

edited

sgouezel commented Dec 25, 2022 •

edited

fpvandoorn left a comment

fpvandoorn Jan 4, 2023

sgouezel Jan 5, 2023

sgouezel Jan 5, 2023

fpvandoorn Jan 5, 2023 •

edited

fpvandoorn Jan 5, 2023 •

edited

sgouezel Jan 6, 2023

bors bot commented Jan 4, 2023

fpvandoorn commented Jan 6, 2023

sgouezel commented Jan 6, 2023

bors bot commented Jan 6, 2023

fpvandoorn commented Jan 6, 2023

sgouezel commented Jan 7, 2023

fpvandoorn commented Jan 7, 2023

bors bot commented Jan 7, 2023

[Merged by Bors] - feat(analysis/convolution): regularity of convolution for functions depending on a parameter #17626

[Merged by Bors] - feat(analysis/convolution): regularity of convolution for functions depending on a parameter #17626

Conversation

sgouezel commented Nov 19, 2022 • edited by github-actions bot

mathlib-dependent-issues-bot commented Dec 2, 2022

fpvandoorn commented Dec 14, 2022

sgouezel commented Dec 15, 2022 • edited by alreadydone

fpvandoorn commented Dec 15, 2022

sgouezel commented Dec 22, 2022 • edited

sgouezel commented Dec 25, 2022 • edited

fpvandoorn left a comment

Choose a reason for hiding this comment

fpvandoorn Jan 4, 2023

Choose a reason for hiding this comment

sgouezel Jan 5, 2023

Choose a reason for hiding this comment

sgouezel Jan 5, 2023

Choose a reason for hiding this comment

fpvandoorn Jan 5, 2023 • edited

Choose a reason for hiding this comment

fpvandoorn Jan 5, 2023 • edited

Choose a reason for hiding this comment

sgouezel Jan 6, 2023

Choose a reason for hiding this comment

bors bot commented Jan 4, 2023

fpvandoorn commented Jan 6, 2023

sgouezel commented Jan 6, 2023

bors bot commented Jan 6, 2023

fpvandoorn commented Jan 6, 2023

sgouezel commented Jan 7, 2023

fpvandoorn commented Jan 7, 2023

bors bot commented Jan 7, 2023

sgouezel commented Nov 19, 2022 •

edited by github-actions bot

sgouezel commented Dec 15, 2022 •

edited by alreadydone

sgouezel commented Dec 22, 2022 •

edited

sgouezel commented Dec 25, 2022 •

edited

fpvandoorn Jan 5, 2023 •

edited

fpvandoorn Jan 5, 2023 •

edited