Zulip Chat Archive

Stream: maths

Topic: Analytic functions


view this post on Zulip 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?

view this post on Zulip Sebastien Gouezel (Apr 25 2020 at 07:31):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (May 02 2020 at 23:33):

The rest is o(x^r).

view this post on Zulip Reid Barton (May 02 2020 at 23:39):

Of course, but try telling Lean that...

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Sebastien Gouezel (May 03 2020 at 07:41):

In Bourbaki, to get a canonical representative, they quotient nn-multilinear functions by the relation: pqp \sim q if p(x,...,x)=q(x,...,x)p (x, ..., x) = q(x, ..., x) for all xx. For instance, in dimension 2, p((x,y),(x,y))=xyp((x, y), (x', y')) = x y' is equivalent to q((x,y),(x,y))=yxq((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))=xyp((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.

view this post on Zulip Yury G. Kudryashov (May 03 2020 at 07:51):

Thank you for the explanation.

view this post on Zulip 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 (x1,...,xn)(x_1, ..., x_n) is σSnp(xσ(1),...,xσ(n))\sum_{\sigma \in S_n} p (x_{\sigma(1)}, ..., x_{\sigma(n)}).

view this post on Zulip David Wärn (May 03 2020 at 07:53):

Is the Bourbaki quotient the same as quotienting by SnS_n?

view this post on Zulip Sebastien Gouezel (May 03 2020 at 07:54):

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

view this post on Zulip Sebastien Gouezel (May 03 2020 at 07:55):

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

view this post on Zulip David Wärn (May 03 2020 at 08:09):

Sebastien Gouezel said:

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

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

view this post on Zulip Sebastien Gouezel (May 03 2020 at 08:36):

Yes, that should do it.


Last updated: May 14 2021 at 20:13 UTC