[Merged by Bors] - feat(Mathlib/Analysis/Analytic): continuously polynomial functions #9269
Conversation
smorel394
added
t-analysis
| theorem HasFiniteFPowerSeriesOnBall.fderiv (h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r) : | ||
| HasFiniteFPowerSeriesOnBall (fderiv 𝕜 f) | ||
| ((continuousMultilinearCurryFin1 𝕜 E F : | ||
| (E[×1]→L[𝕜] F) →L[𝕜] E →L[𝕜] F).compFormalMultilinearSeries | ||
| (p.changeOriginSeries 1)) | ||
| x n r := by |
There was a problem hiding this comment.
I know you probably adapted the proof of the existing HasFPowerSeriesOnBall.fderiv (which assumes CompleteSpace), but I wonder why that statement doesn't use FormalMultilinearSeries.shift ... I think we should look into proving they are equal.
Once we have this, I think the main goal of #9130 can be achieved by identifying shift with linearDeriv in the case of a FormalMultilinearSeries of a single term, right? We should probably add it the equality to the other file after this is merged.
There was a problem hiding this comment.
I know you probably adapted the proof of the existing HasFPowerSeriesOnBall.fderiv (which assumes CompleteSpace), but I wonder why that statement doesn't use FormalMultilinearSeries.shift ... I think we should look into proving they are equal.
I don't think that they are equal. I tried proving that they are, and the expression used in HasFPowerSeriesOnBall.fderiv seems to scramble the variables more, as well as having an extra factor of n+1 in degree n. The first point would not be surprising, as the only thing we know about the two formal multilinear series is that they have the same sum, which does not determine them (unless they are symmetric and we are in characteristic zero). The second point... well, are we sure that FormalMultilinearSeries.shift really is the Taylor series of the derivative ? The mathlib file says that it is but doesn't give any explanation or reference. I'll need a pen and paper to investigate more.
Once we have this, I think the main goal of #9130 can be achieved by identifying
shiftwithlinearDerivin the case of a FormalMultilinearSeries of a single term, right? We should probably add it the equality to the other file after this is merged.
I would be happy to make the definition of linearDeriv look more natural, but I don't understand what you mean here. What is a FormalMultiliearSeries of a single term, and how would you adapt the definition of shift so that it applies in the context of #9130, where you're working with multilinear maps ? Or do you mean that we should prove that the FormalMultilinearSeries of f.linearDeriv is equal to the shift of the FormalMultilinearSeries of f ? (I'm not sure that's true though.)
By the way, I started rewriting the next step, i.e. the proof that continuous multilinear maps are analytic, there. The things I am using so far fro #9130 are domDomRestrict, toFormalMultilinearSeries_fixedDegree (and its lemmas) and toFormalMultilinearSeries_partialSum. It totally forgot about linearDeriv, I should probably prove that it is indeed the Fréchet derivative...
There was a problem hiding this comment.
So what should I do with this suggestion ? As I said, FormalMultilinearSeries.shift is not equal to the formal power series of the derivative that is currently in mathlib. There are two issues:
(1) Formal power series are not unique, so we could at most expect the two formal power series to coincide on the diagonal. This is not a big issue, as we only care about the behavior on the diagonal, but if we want to use shift it means rewriting a pretty big proof.
(2) The normalization: usually Taylor series of functions have factors shift was defined with that normalization in mind. So if it is to be the formal power series of the derivative, its definition has to be changed, preferably with a comment explaining why. (Problem: I don't know what that would break.)
So in the end, it is probably possible to do something using a modified version of FormalMultilinearSeries.shift, but I'm not sure that it would justify the extra effort, because I don't know what we would gain. We already know that, if f is continuously polynomial of degree n, then its derivative is continuously polynomial of degree n-1. We can get more explicit formulas for f'(x) in particular cases using the degree 1 term of the formal multilinear series of f at x; I did that for continuous multilinear maps, for example.
There was a problem hiding this comment.
Thanks. I looked into the definition of shift and it seems to be only currying the last coordinate, so it could only possibly work for a series whose terms are all symmetric multilinear forms. Even in that case, the nth term seems to be missing a factor of n. I think we should remove the claim that it's the derivative from the docstring.
Regarding the connection with linearDeriv, maybe the most general thing we can state and prove is that linearDeriv evaluate to the same thing as the changeOriginSeries 1 of toFormalMultilinearSeriesFixedDegree. (Regarding the definition of toFormalMultilinearSeriesFixedDegree: I think you need to sum over powersetCard because you want a series development around an arbitrary point, but I think you can just define the series around the origin, which would just be a single term (a "homogeneous" CPolynomial), and then use changeOrigin of FormalMultilinearSeries rather than repeating the work.)
There was a problem hiding this comment.
I tracked down the history and it appears the claim that FormalMultilinearSeries.shift is the derivative was added in mathlib3#2012 originally. Do you agree the claim is problematic, @sgouezel?
There was a problem hiding this comment.
@smorel394, could you have a look at #9373 to see if you think the clarification of the docs is good enough for you, or if you think you can make it even better for future users?
There was a problem hiding this comment.
It looks good to me.
There was a problem hiding this comment.
Regarding the connection with linearDeriv, maybe the most general thing we can state and prove is that
linearDerivevaluate to the same thing as thechangeOriginSeries 1oftoFormalMultilinearSeriesFixedDegree. (Regarding the definition oftoFormalMultilinearSeriesFixedDegree: I think you need to sum over powersetCard because you want a series development around an arbitrary point, but I think you can just define the series around the origin, which would just be a single term (a "homogeneous" CPolynomial), and then use changeOrigin of FormalMultilinearSeries rather than repeating the work.)
This is really about PR #9130, I'm making changes there to answer your suggestion.
There was a problem hiding this comment.
Done, I've also rewritten the proof that continuous multilinear maps are analytic in another project. The applications to differentiability require completeness right now, but only until this PR is merged.
I got rid of the formal multilinear series stuff in #9130, since the definition of the formal multilinear series at 0 is so basic and can be done very quickly when needed. The proof that the fderiv is equal to the degree 1 of changeOrigin of the formal multilinear series at 0 is a bit messy for now, but at least it compiles, and I'm sure I can make it shorter.
There was a problem hiding this comment.
I've now shown that if a function has any power series on a ball, then its Taylor series (with the 1/n! factor) does converge to the function on the ball, here on Zulip. However, in order to show that the Taylor series satisfies the HasFPowerSeriesOnBall perdicate, we need to bound the growth of the norms of the terms in the series, which would require a polarization identity.
alreadydone
changed the title
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
…ial" stuff in another file.
leanprover-community-mathlib4-bot
added
the
merge-conflict
|
Yeah it was the import in Calculus.FDeriv.Analytic, wasn't it. I finally figured it out, but looks like you got there just before me... |
|
I think you also need to add the CPolynomial file to Mathlib.lean. |
|
Oh, is that something that you need to do every time you add a new file ? Good to know. |
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
If you click on the second "detail" you'll be led to this page which shows what needs to be done. I think the bot used to suggest such fixes ... |
|
I did click on the "details" page, but I didn't see any information that I could understand... |
|
Yes it's not totally clear. It's presented in the form of a diff for you to apply, like the bot's suggestion. |
|
Also, CI still fails, and the bot seems to be suggesting that I remove CPolynomial from Mathlib.lean, or switch the order? It's making several suggestions and they don't seem very compatible. |
Okay, well, now I see what you mean, but there was no way I was going to understand that on my own... I guess I'll know next time. |
|
So let's see if I understand the suggestion this time. I think it wants me to move a line around. I thought the imports were in alphabetical order, but apparently not. |
|
✌️ smorel394 can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-mathlib4-bot
added
delegated
and removed
awaiting-review
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Johan Commelin <johan@commelin.net>
|
bors r+ |
…9269) This defines "continuously polynomial" (shortened to "cpolynomial") functions as a special cases of analytic functions: they are the functions that admit a development as a *finite* formal multilinear series. Then we prove their basic properties. The point of doing is this is that finite series are always summable, so we can remove the completeness assumptions in some results about analytic functions (differentiability for example). Examples of continuously polynomial functions include continuous multilinear maps, and functions defined by polynomials. Co-authored-by: smorel394 <67864981+smorel394@users.noreply.github.com> Co-authored-by: morel <smorel@math.princeton.edu>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
This defines "continuously polynomial" (shortened to "cpolynomial") functions as a special cases of analytic functions: they are the functions that admit a development as a finite formal multilinear series. Then we prove their basic properties. The point of doing is this is that finite series are always summable, so we can remove the completeness assumptions in some results about analytic functions (differentiability for example). Examples of continuously polynomial functions include continuous multilinear maps, and functions defined by polynomials.