Inversion is analytic

Stream: maths

[Heather Macbeth]

Given equivalent Banach spaces E and F, the subset U = (E ≃L[𝕜] F) of E →L[𝕜] F consisting of invertible operators is open. As far as I can tell, this fact is necessary to prove the inverse function theorem in the $C^k$ and smooth categories.

I cannot see how to prove this fact without more machinery. @Sebastien Gouezel @Yury G. Kudryashov (and others), here is what I can think of; can you streamline it?

normed_space.multilinear : In a Banach algebra A, the symmetrized diagonal map $(a_1, ... a_n) \mapsto \sum_{\sigma\in S_n}a_{\sigma(1)}\cdots a_{\sigma(n)}$ is multilinear.
calculus.times_cont_diff : Define a formal power series in a Banach algebra A. This induces a formal multilinear series.
analytic.[new file] : Theory of Banach-algebra-analytic functions, i.e., analytic functions whose formal multilinear series is a formal power series in a Banach algebra. Series $1 + a + a^2 + \cdots$ for $(1-a)^{-1}$; hence, analyticity of the inversion function, and the openness of the group of units. Compare issue #1858
normed_space.operator_norm : E →L[𝕜] E (fixed typo, had written E →L[𝕜] F) is a Banach algebra.

[Sebastien Gouezel]

You can indeed give a proof using the fact that E →L[𝕜] E is a Banach algebra. If you need shortcuts, you can also give a pretty direct proof, by noting that if A is invertible, then you have an inverse for A + h for small enough h, given by the series $\sum (-A^{-1} h)^n A^{-1}$ (where the convergence follows from the norm convergence, which follows from the convergence of geometric series -- and all this is already in mathlib).

[Heather Macbeth]

Is that ok? You said at the discussion of #1858,

I just want to get the definition of analytic functions in Lean because this is so basic and too easy to do in the non-proper generality.

so I suspect you would prefer to have facts about analytic functions in Banach algebras also done in their proper generality :)

[Patrick Massot]

He meant "including the case of $p$-adic analytic functions" and stuff like that.

[Patrick Massot]

:shrug:

[Kevin Buzzard]

I think k should be a complete Banach algebra in this lemma, so we can apply the result in the theory of adic spaces :P

[Heather Macbeth]

I guess the question here is whether the theory of power series in a Banach algebra should be set up as a special case of Sebastien's theory of formal multilinear series. In the long term, surely yes; in the short term, ...?

[Sebastien Gouezel]

Power series in a Banach algebra is more like (one-dimensional) complex analysis. This situation deserves a whole independent API (just like we have one for the one-dimensional derivative). The higher dimensional results can be applied to this specific situation (for instance to deduce that the composition of analytic functions is analytic, or things like that).

[Heather Macbeth]

Yes. But in mathlib, we have deriv defined in terms of fderiv. I am asking whether we should do the analogue here ...

[Heather Macbeth]

... i.e., to define a Banach-algebra-analytic function as one which is (in your current definition)-analytic with respect to the formal multilinear series induced by some formal power series.

[Kevin Buzzard]

I wasn't being serious. But the reason I said it is that actually I once wrote 30 pages about the basic theory of compact maps between modules over a Banach algebra, and characteristic power series etc etc, because I needed it all in the p-adic case when I was working with p-adic families of automorphic forms. I was generalising work of Coleman (which was inaccurate in places); Coleman himself told me that he was proud, because he was generalising work of Grothendieck, something which is essentially impossible due to the way Grothendieck worked (but this was early Grothendieck).

[Sebastien Gouezel]

analytic is already defined, so it doesn't need a new definition. The equivalence with the other definition in terms of (usual) power series will have to be proved, yes, but it doesn't have to be now. Just having a stub of a theory with what you need now definitely makes sense, though!

[Heather Macbeth]

Let me check I understand correctly: there is currently no definition of what I am calling a Banach-algebra-analytic function, right? That is, a function from a Banach algebra to itself locally equal to a power series $a \mapsto \sum_{i=0}^\infty c_ia^i$.

[Sebastien Gouezel]

Exactly.

[Heather Macbeth]

What is currently defined in analytic is a function locally equal to a formal multilinear series $a \mapsto \sum_{i=0}^\infty C_i(a,a,\ldots a)$, where $C_i$ are $i$-multilinear maps that have no particular connection to the Banach algebra structure.

[Sebastien Gouezel]

Yes.

[Heather Macbeth]

OK, thanks! So you are suggesting I do just the stub of the power series theory, and for now, not establish the relationship to the more general theory?

[Heather Macbeth]

@Kevin Buzzard maybe you can do the most general version for us :)

[Kevin Buzzard]

It is somehow impossible, isn't it. I am pleased that all this stuff is being set up in this generality, because p-adic Banach spaces are objects which have been seriously used in number theory (even Serre wrote a paper about them in the 60s, related to the Weil conjectures), but one can always find more generality; at some point you have to know when to stop.

[Sebastien Gouezel]

Yes, it seems reasonable. Although if you start needing results that would follow from the general theory (like, the composition or the inverse of analytic maps is analytic), it is better to prove the relationship with the general theory than to prove them again in your specific case.

[Heather Macbeth]

OK. Thanks a lot. It may be possible to avoid the general theory, for now. Dieudonné in Foundations of modern analysis uses power series only to show that the set of invertible operators is open; then he has a clever induction to show that the inversion operation is smooth, without ever having proved that it is analytic.