[Merged by Bors] - feat: bundled C^n maps supported in a fixed compact set#30197
[Merged by Bors] - feat: bundled C^n maps supported in a fixed compact set#30197luigi-massacci wants to merge 17 commits intoleanprover-community:masterfrom
Conversation
PR summary 928504d552Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
grunweg
left a comment
There was a problem hiding this comment.
Thanks for getting this work started! Here are a first few minor comments (just about the docs so far).
Most importantly, this file defines a type of bundled functions (while we often use unbundled functions in mathlib). Can you mention why we do this, namely because this will be related to the space of test functions for defining distributions? Thanks!
|
Should this PR be Co-authored-by: Anatole (or perhaps, adding an empty commit with him as the author)? |
The commit should already be there? It's 64effd6. But let me add it to the text description too to be clear. |
| /-- The underlying function. Use coercion instead. -/ | ||
| protected toFun : E → F | ||
| protected contDiff' : ContDiff ℝ n toFun | ||
| protected zero_on_compl' : EqOn toFun 0 Kᶜ |
There was a problem hiding this comment.
I would have expected this condition to be tsupport toFun ⊆ K. Is that more annoying to use?
There was a problem hiding this comment.
The choice to write it that way was made by @ADedecker a long time ago, maybe he has a more sophisticated explanation, but for myself, I certainly found it very convenient when working with integrals as it makes it much more direct to rewrite (eg: turn an integral over E to one over just K, etc), and my impression is that tsupport was a bit more awkward to use, though that might be be only an argument in favor of adding more API
There was a problem hiding this comment.
Yes, this is precisely the point: while those are only a few rewrites away, this is the condition which is most elementary to manipulate IMHO. One key point is that we don't want to be constantly rewriting between tsupport toFun ⊆ K and support toFun ⊆ K (using that K is closed).
Now, looking at the current state at the API for tsupport I can see that it is indeed much better than it was a few years ago (e.g we have docs#tsupport_iteratedFDeriv_subset), but I still think that this condition will be more natural in general.
Of course this could just be solved with API, so if you really prefer the definition to be in terms of tsupport this can be changed.
|
|
||
| /-- The type of `n`-times continuously differentiable maps which vanish outside of a fixed | ||
| compact `K`. -/ | ||
| structure ContDiffMapSupportedIn (n : ℕ∞) (K : Compacts E) : Type _ where |
There was a problem hiding this comment.
Here I would have assumed that we define it for arbitrary subsets and just use the assumption that K is compact whenever that is actually needed.
There was a problem hiding this comment.
I'm not opposed to it, but I think the answer to "wherever it is actually needed" is "everywhere". Certainly the topology requires compactness. If K is not compact I'm not sure there is a lot more value in defining a separate structure (on which one can pile on instances) as opposed to just using ContDiffOn on an unbundled function.
There was a problem hiding this comment.
I think the main point was indeed instances, because typeclass search does not work with extra non-instance parameters. Of course you could assume [CompactSpace K], but I think this is a bit artificial.
Also, note that people will essentially never (I think?) have K be their favourite compact set: this will appear in the continuity criterion for distributions, so either you will have to work with arbitrary K : Compacts E or with a specific element of an exhaustion, both of which have essentially been proven compact already at this point.
(Although maybe we should make the FunLike instance of CompactExhaustion land in Compacts to make this even easier, but this can wait)
grunweg
left a comment
There was a problem hiding this comment.
I took another pass over the code: just very minor comments (and one question for my own understanding).
grunweg
left a comment
There was a problem hiding this comment.
Can you fix my two style comments and perhaps use inherit_doc, and then this is good?
maintainer delegate
|
I decided to be slightly pushy and applied my style tweaks myself. Feel free to revert any that you disagree with! |
|
maintainer delegate |
|
🚀 Pull request has been placed on the maintainer queue by grunweg. |
|
bors d+ |
|
✌️ luigi-massacci can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
Add a type of n-times continuously differentiable maps supported in a fixed compact set and related notation. Co-authored by: @ADedecker Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com> Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
|
Pull request successfully merged into master. Build succeeded: |
…ommunity#30197) Add a type of n-times continuously differentiable maps supported in a fixed compact set and related notation. Co-authored by: @ADedecker Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com> Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
Add a type of n-times continuously differentiable maps supported in a fixed compact set and related notation.
Co-authored by: @ADedecker