[Merged by Bors] - feat: update the ContDiff definition to integrate analytic functions in the hierarchy
#17152
Conversation
For this, move the results needing `ContDiff` to two new files. The reason of this change is that I will import `FDeriv.Analytic` in `ContDiff.Defs` in #17152
mathlib4-dependent-issues-bot
removed
the
blocked-by-other-PR
| variable [CompleteSpace 𝕜] | ||
|
|
||
|
|
| @@ -579,7 +579,7 @@ theorem _root_.DifferentiableOn.analyticOn {s : Set ℂ} {f : ℂ → E} (hd : D | |||
| differentiable on `s`. -/ | |||
| protected theorem _root_.DifferentiableOn.contDiffOn {s : Set ℂ} {f : ℂ → E} {n : ℕ} | |||
| (hd : DifferentiableOn ℂ f s) (hs : IsOpen s) : ContDiffOn ℂ n f s := | |||
| (hd.analyticOnNhd hs).contDiffOn | |||
| (hd.analyticOnNhd hs).contDiffOn hs.uniqueDiffOn | |||
There was a problem hiding this comment.
Why AnalyticOnNhd.contDiffOn needs UniqueDiffOn now? UPD: I see that this is required for n = ω but this lemma takes n : Nat. Should it be upgraded to n : WithTop ENat?
There was a problem hiding this comment.
The assumptions in AnalyticOnNhd.contDiffOn have changed: in the previous version, it was requiring a complete space, but no unique differentiability. While the new version drops completeness, but requires unique differentiability.
There was a problem hiding this comment.
Does it make sense to have the old version too? Anyway, could you please mention API changes like this one (i.e., not just ENat -> WithTop ENat) in the commit message? Also, am I right that we can upgrade this lemma from n : Nat to n : WithTop ENat for free?
There was a problem hiding this comment.
Sure, I've added back the old version, under the name AnalyticOnNhd.contDiffOn_of_completeSpace (and I've used it in CauchyIntegral.lean).
I think the new lemma already uses n : WithTop ENat.
leanprover-community-bot-assistant
added
the
merge-conflict
leanprover-community-bot-assistant
removed
the
merge-conflict
| @@ -579,7 +579,7 @@ theorem _root_.DifferentiableOn.analyticOn {s : Set ℂ} {f : ℂ → E} (hd : D | |||
| differentiable on `s`. -/ | |||
| protected theorem _root_.DifferentiableOn.contDiffOn {s : Set ℂ} {f : ℂ → E} {n : ℕ} | |||
There was a problem hiding this comment.
Will it work like this?
| protected theorem _root_.DifferentiableOn.contDiffOn {s : Set ℂ} {f : ℂ → E} {n : ℕ} | |
| protected theorem _root_.DifferentiableOn.contDiffOn {s : Set ℂ} {f : ℂ → E} {n : WithTop ℕ +} |
|
Otherwise LGTM. Thanks! |
|
✌️ sgouezel can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
leanprover-community-mathlib4-bot
added
the
ready-to-merge
…s in the hierarchy (#17152) We modify the definition of `ContDiff` so that the smoothness exponent belongs to `WithTop (ℕ∞)`, where top smoothness (denoted with `ω` in the `ContDiff` scope) means analyticity (together with analyticity of all the iterated derivatives). This will make it possible to write theorems like: consider a function which is `C^2` over the reals or complexes, or analytic over a general field. Then... Many theorems in calculus hold under these assumptions (and it's the way things are written in Bourbaki), so having this possibility is a necessary improvement unless one wants to duplicate everything. The PR is mostly not changing the API: theorems that were proved for `C^n` functions with `n ∈ ℕ or n = ∞` are now proved for `n ∈ ℕ or n = ∞ or n = ω` (unless they are not true for analytic functions, but it turns out in most cases things are fine). Of course, results have to be added in the files `ContDiff.Def` and `ContDiff.Basic` to deal with analytic functions. I know that the PR is huge and hard to review. I have tried to separate all the other results in other PRs, but once one changes the basic definition one has to fix everything downstream to get mathlib compiling, so I can not make it shorter... Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
ContDiff definition to integrate analytic functions in the hierarchyContDiff definition to integrate analytic functions in the hierarchy
We modify the definition of
ContDiffso that the smoothness exponent belongs toWithTop (ℕ∞), where top smoothness (denoted withωin theContDiffscope) means analyticity (together with analyticity of all the iterated derivatives).This will make it possible to write theorems like: consider a function which is
C^2over the reals or complexes, or analytic over a general field. Then... Many theorems in calculus hold under these assumptions (and it's the way things are written in Bourbaki), so having this possibility is a necessary improvement unless one wants to duplicate everything.The PR is mostly not changing the API: theorems that were proved for
C^nfunctions withn ∈ ℕ or n = ∞are now proved forn ∈ ℕ or n = ∞ or n = ω(unless they are not true for analytic functions, but it turns out in most cases things are fine). Of course, results have to be added in the filesContDiff.DefandContDiff.Basicto deal with analytic functions.I know that the PR is huge and hard to review. I have tried to separate all the other results in other PRs, but once one changes the basic definition one has to fix everything downstream to get mathlib compiling, so I can not make it shorter...
∑ n, n * r ^ n#15270AnalyticWithinAtwithContDiffWithinAt#16725AnalyticWithinAt#16843change originpart fromAnalytic.Basic#16891Analyticfolder #16972HasSummableGeomSeriesto unify results between normed field and complete normed algebras #17002AnalyticOntoAnalyticOnNhd, andAnalyticWithinOntoAnalyticOn#17146WithTop ℕ∞#17164C^nfunctions isC^n#18722HasFTaylorSeriesto take a parameter inWithTop ℕ∞instead ofℕ∞#18723ContDiff.DefsinFDeriv.Analytic#19374ContDiffto take a smoothness exponent inWithTop ℕ∞#19442