Analytic functions

Stream: maths

[Yury G. Kudryashov]

@Sebastien Gouezel Do I understand correctly that currently we have two types of formal series in mathlib: finite dimensional version sharing monomials with mv_polynomial and those used in Taylor series? Are there any bridges?

[Sebastien Gouezel]

Yes, we have these two versions, and I don't think there are any bridges yet.

[Yury G. Kudryashov]

@Sebastien Gouezel I stopped understanding why analytic functions / power series need lots of combinatorics for theorems like associativity. The space of formal series is the projective (?) limit of the spaces of r-jets. In each space associativity is trivial because it holds for functions representing these r-jets, and the r-jet of f ∘ g is determined by r-jets of f and g.
Is there something wrong with this proof?

[Reid Barton]

I think the last bit (r-jet of composition is determined by the r-jets) might not be so trivial to prove, if it isn't proved already

[Yury G. Kudryashov]

The rest is o(x^r).

[Reid Barton]

Of course, but try telling Lean that...

[Reid Barton]

But it's probably still a lot easier than whatever is there now (I haven't looked at the PR yet).

[Sebastien Gouezel]

The thing is that the multilinear series is not determined uniquely by the function: it would be if you required additionally that the terms in the mulitlinear expansion are symmetric multilinear functions, but you can not require this in general in positive characteristic. So, the truncated series is not the r-jet of the function. In particular, when you define composition of multilinear series, there is some choice involved (you could permute arbitrarily the variables, and you would still have a multilinear series for the composition of the analytic functions), but with a random choice associativity of composition would not be true. With the canonical choice (enumerate all variables in increasing order), associativity of composition is true, but it requires a proof.

[Sebastien Gouezel]

In Bourbaki, to get a canonical representative, they quotient $n$-multilinear functions by the relation: $p \sim q$ if $p (x, ..., x) = q(x, ..., x)$ for all $x$. For instance, in dimension 2, $p((x, y), (x', y')) = x y'$ is equivalent to $q((x, y), (x', y')) = y x'$ (but in characteristic 2 those don't have a symmetric representative). Since it doesn't bring concrete improvements and makes everything more complicated to state and prove, I have not implemented this. In this example $p((x, y), (x', y')) = x y'$ in characteristic 2, note that the second derivative of the function is zero, but the second term in the power series expansion is not zero.

[Yury G. Kudryashov]

Thank you for the explanation.

[Sebastien Gouezel]

One thing that I should do (and haven't done yet) is prove that, if the n-th term in the power series expansion is p, then the n-th derivative applied to $(x_1, ..., x_n)$ is $\sum_{\sigma \in S_n} p (x_{\sigma(1)}, ..., x_{\sigma(n)})$.

[David Wärn]

Is the Bourbaki quotient the same as quotienting by $S_n$?

[Sebastien Gouezel]

No. For instance, $p((x, y), (x',y')) = x y' - y x'$ is equivalent to $0$.

[Sebastien Gouezel]

I just noticed how latex is nicer than backquotes in Zulip :)

[David Wärn]

Sebastien Gouezel said:

No. For instance, $p((x, y), (x',y')) = x y' - y x'$ is equivalent to $0$.

I think you would need to quotient by span of $p - \sigma p$, not just identify $p = \sigma p$

[Sebastien Gouezel]

Yes, that should do it.