# Zulip Chat Archive

## Stream: maths

### Topic: Analytic functions

#### Yury G. Kudryashov (Apr 25 2020 at 07:29):

@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 (Apr 25 2020 at 07:31):

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

#### Yury G. Kudryashov (May 02 2020 at 22:15):

@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 (May 02 2020 at 22:39):

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 (May 02 2020 at 23:33):

The rest is `o(x^r)`

.

#### Reid Barton (May 02 2020 at 23:39):

Of course, but try telling Lean that...

#### Reid Barton (May 02 2020 at 23:42):

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

#### Sebastien Gouezel (May 03 2020 at 07:25):

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 (May 03 2020 at 07:41):

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 (May 03 2020 at 07:51):

Thank you for the explanation.

#### Sebastien Gouezel (May 03 2020 at 07:53):

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 (May 03 2020 at 07:53):

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

#### Sebastien Gouezel (May 03 2020 at 07:54):

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

#### Sebastien Gouezel (May 03 2020 at 07:55):

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

#### David Wärn (May 03 2020 at 08:09):

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 (May 03 2020 at 08:36):

Yes, that should do it.

Last updated: May 14 2021 at 20:13 UTC