[Merged by Bors] - feat(analysis/calculus/cont_diff): Prove that fderiv_within is C^n for functions with parameters#16946
[Merged by Bors] - feat(analysis/calculus/cont_diff): Prove that fderiv_within is C^n for functions with parameters#16946fpvandoorn wants to merge 35 commits intomasterfrom
fderiv_within is C^n for functions with parameters#16946Conversation
fderiv_within is C^n for functions with parameters
src/analysis/calculus/cont_diff.lean
Outdated
| (hf : cont_diff_within_at 𝕜 (n+1) (function.uncurry f) u (x, g x)) | ||
| (hg : cont_diff_within_at 𝕜 n g s x) | ||
| (hst : insert x s ×ˢ t ⊆ u) -- can be weakened to only consider points near `(x, g x)` | ||
| (hu : u ∈ 𝓝[(λ x, (x, g x)) '' s] (x, g x)) : |
There was a problem hiding this comment.
| (hu : u ∈ 𝓝[(λ x, (x, g x)) '' s] (x, g x)) : | |
| (hu : u ∈ 𝓝[(λ x', (x', g x')) '' s] (x, g x)) : |
Also, I feel that this assumption is pretty weird. Isn't it more natural to assume, say, that g maps s to t? (which should imply your assumption by hst, but most importantly feels like a natural assumption for the lemma). If you agree with that, maybe you can even ditch completely u, and assume instead of hf that f is C^{n+1} on insert x s ×ˢ t?
There was a problem hiding this comment.
Yes, I think I can ditch u.
In the application I don't have that g maps s to t.
I want to conclude that mfderiv with some appropriate coordinate change is smooth. The definition of mfderiv uses (fderiv_within 𝕜 ... (range I) (ext_chart_at I x x). Whatever my g is in my application, it is not well-behaved everywhere on range I, just on the target of some chart. So I only want a local property on g.
The property I gave was the weakest one I found to still prove the result. Maybe I can do something less-crazy looking (e.g. sending a neighborhood of x within s to t)?
There was a problem hiding this comment.
Ok, I made some changes:
- I removed
uand required thatfis smooth oninsert x s ×ˢ t, as you suggested - I replaced the weird-looking condition with
t ∈ 𝓝[g '' s] g x₀, which seems more natural. - Note that the condition you suggested, that
gmapsstot, is precisely assumed in the special casecont_diff_within_at.fderiv_within'. However, as mentioned in my previous message, I also need this more general case.
sgouezel
left a comment
There was a problem hiding this comment.
LGTM, modulo a few docstrings
bors d+
I'm sure I don't need to tell you this, but still: please don't forget the corresponding mathlib 4 PR.
|
✌️ fpvandoorn can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Thanks for the synchronization reminder, I might have forgotten it. It is leanprover/mathlib4#1833 |
|
bors merge |
…` for functions with parameters (#16946) * Prove that `fderiv_within` is `C^n` (at a point within a set) for a function with parameters * There are some inconvenient side-conditions needed for the lemmas, feel free to recommend improvements * `set.diag_image` is not used, but a (useful) left-over used before a refactor. * This is useful for lemmas about `mfderiv` and the smooth vector bundle refactor * From the sphere eversion project
|
Pull request successfully merged into master. Build succeeded: |
fderiv_within is C^n for functions with parametersfderiv_within is C^n for functions with parameters
leanprover-community/mathlib3#16946 Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
fderiv_withinisC^n(at a point within a set) for a function with parametersset.diag_imageis not used, but a (useful) left-over used before a refactor.mfderivand the smooth vector bundle refactor