Formal power series on `ι -> R`

Stream: mathlib4

[Yury G. Kudryashov]

Do we have API for a docs#MvPowerSeries - like constructor for docs#FormalMultilinearSeries ?
I want to formalize the multivariate Cauchy integral formula using docs#torusIntegral, and I need a constructor that takes (ι →₀ R) → E and creates a formal multilinear series using sum over antidiagonal and Finsupp.prod.

[Yury G. Kudryashov]

If the answer is "no" (I suspect that this is the case), then I'll work on this over this week-end.

[Yury G. Kudryashov]

More details: I need to prove that $\frac{1}{(2\pi i)^n}\oiint_{\{\zeta : \mathbb C^n \mid \forall i, |\zeta_i-c_i|=R\}}\frac{f(\zeta)-f(z)}{\prod_i(\zeta_i-z_i)}d\zeta_1..d\zeta_n$ is analytic in z in ball c R.

[Yury G. Kudryashov]

I see two options:

• explicitly define the formal power series and prove its convergence;
• somehow reuse facts about analyticity of the composition.

[Yury G. Kudryashov]

With the first approach, I will have to effectively redo some lemmas about composition. With the second approach, I will need a predicate saying that not only a series converges on a ball but we have a specific estimate on the rate of convergence.

[Yury G. Kudryashov]

@Sebastien Gouezel What do you think?

[Sebastien Gouezel]

In general, knowing that a function is analytic on a ball of radius r does not imply that its coefficients grow at most like r^{-n} (this is true over the complex, but not over the real, and this is generally deduced from Cauchy integral formula). This means that explicit estimates on composition will typically not behave as well as one could expect naively.

This does not really answer your question, but it's because I haven't really understood the question, sorry.

[Yury G. Kudryashov]

I'm sorry for badly formulating my question. For the second approach, I thought about introducint a predicate HasFPowerSeriesOnWith that takes an extra argument C and claims that the norm of each k-linear component is at most C / r ^ k.

[Yury G. Kudryashov]

Then HasFPowerSeriesOn .. R will imply ∀ r < R, ∃ C, HasFPowerSeriesOnWith .. r C.

[Yury G. Kudryashov]

But we can have lemmas like "if a family of functions is uniformly analytic on a ball, then the limit/integral/... is analytic as well"

[Yury G. Kudryashov]

The first approach is to provide an explicit formula for the series.

[Antoine Chambert-Loir]

Isn't this an instance of a general result about analyticity of integrals wrt parameters? Over C, one can go via holomorphy, over the reals, I'd use the result over C. Over other fields, I'd look at what Bourbaki wrote, but I fear that it requires some algebra of the kind you suggest.

[Yury G. Kudryashov]

What do you mean by "Over C, one can go via holomorphy"?

[Yury G. Kudryashov]

I need this to prove that differentiability implies analyticity in case of a domain of an arbitrary finite dimension.

[Antoine Chambert-Loir]

Oh, sorry for the circularity... I'll look at Cartan an Demailly 's books.

[Antoine Chambert-Loir]

I have Cartan's book Théorie élémentaire des fonctions analytiques d'une ou plusieurs variables complexes on my table. This theorem you wish to prove is chapter IV, §5, on page 135. It is done by first showing the representation formula that you hinted at (proposition 2.1; actually, he contents himself with the case of two variables). Then (proposition 3.1), he proves the power series expansion, by expanding under the integral sign, showing normal convergence, termwise integration and he gets the expansion, with an explicit formula.

[Yury G. Kudryashov]

BTW, is there some form of this theorem (differentiable -> analytic) for an infinite-dimensional codomain?

[Antoine Chambert-Loir]

You mean, beyond the case where the bidual morphism of the codomain is an isomorphism?

[Antoine Chambert-Loir]

Yury G. Kudryashov said:

BTW, is there some form of this theorem (differentiable -> analytic) for an infinite-dimensional codomain?

Bourbaki, VAR (Fascicule de résultats sur les variétés différentiables) asserts something like that for functions defined on an open subset of a finite dimensional complex vector space $E$, with values in a complex topological vector space which is locally convex and quasi-complete (meaning every closed and bounded subset is complete,
EVT III, §2, n° 5). Reflexive Banach spaces, with their weak topology, are examples.

[Yury G. Kudryashov]

Oh, I made a typo: codomain instead of domain.

[Yury G. Kudryashov]

For codomains, Banach spaces work for me (for now), we can generalize later if needed.

[Antoine Chambert-Loir]

For infinite dimensional domain, the canonical reference is Douady (1966), Le problème des modules pour les sous-espaces analytiques compacts d'un espace analytique donné, who works with a definition of analytic spaces modeled on analytic subspaces of complex Banach spaces. (Note that this is more general than what mathlib currently allows to define because these analytic subspaces are not necessarily reduced. )

The definition is carefully done and starts with the notion of polynomial map $E\to F$ where $E$ and $F$ are Banach spaces.

http://www.numdam.org/articles/10.5802/aif.226/

[Antoine Chambert-Loir]

(Actually, this is a special case of the notion of polynomial map $M \to N$ between two modules over a commutative ring $R$ which is currently being formalized by @María Inés de Frutos Fernández and myself. The fact that he works over $\mathbf R$ (or $\mathbf C$) simplifies the definition.)

[Sebastien Gouezel]

A reference I like a lot is Mujica, Complex analysis in Banach spaces.