# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: Exponential

#### Ashvni Narayanan (Dec 16 2020 at 16:21):

Is there a file which describes `real.exp^x`

as a `tsum`

or `sum`

?

Any help is appreciated, thank you!

#### Eric Wieser (Dec 16 2020 at 16:24):

~~Perhaps something near src#complex.exp'?~~

#### Kevin Buzzard (Dec 16 2020 at 16:25):

What do you mean by `real.exp^x`

? Do you just mean `real.exp`

?

#### Ashvni Narayanan (Dec 16 2020 at 16:28):

Yes, sorry, I mean the Taylor series corresponding to `e^x`

where `e`

is `real.exp`

#### Johan Commelin (Dec 16 2020 at 16:28):

No, `exp`

is the function, not the number

#### Johan Commelin (Dec 16 2020 at 16:29):

`real.exp x`

$= e^x$

#### Heather Macbeth (Dec 16 2020 at 16:30):

AFAIK, not currently, but @Yury G. Kudryashov is working on a refactor that will allow for this.

#### Heather Macbeth (Dec 16 2020 at 16:30):

Why do you need it?

#### Ashvni Narayanan (Dec 16 2020 at 16:32):

I'm trying to prove the following lemma :

```
lemma exp_bernoulli_neg : ∀ t : ℚ, ((∑' i : ℕ, ((bernoulli_neg i) : ℚ) * t^i / (nat.factorial i)) : ℝ) * (real.exp t - 1) = t :=
```

where `bernoulli_neg i`

is the ith Bernoulli number.

#### Kevin Buzzard (Dec 16 2020 at 16:33):

You would be better off proving a theorem about formal power series than worrying about convergence of real power series here

#### Kevin Buzzard (Dec 16 2020 at 16:33):

We have formal power series in Lean

#### Heather Macbeth (Dec 16 2020 at 16:43):

Kevin, I guess that depends on whether Ashvni needs an identity of formal power series or an identity about real functions. (But maybe you know her intended application?)

#### Kevin Buzzard (Dec 16 2020 at 16:55):

Indeed I do :-)

#### Kevin Buzzard (Dec 16 2020 at 16:58):

I think that the formal power series identity will boil down to checking a fact about Bernouilli numbers which she already knows (because she showed me a proof last week), whereas checking the real identity will involve a whole lot of kerfuffle ultimately reducing to checking the formal power series identity. What do you think Ashvni? The definition of formal power series multiplication and the fact that two formal power series are equal iff they have the same coefficients should reduce you directly to something you know already, with the advantage that you can stay working over the rationals.

#### Kevin Buzzard (Dec 16 2020 at 17:00):

I think this raises a more general question about "formal exponentiation", which has come up before. In stuff like p-adic analysis one still has exponentiation `exp x`

and logarithm `log (1 + x)`

but they're defined by formal power series (and of course the radius of convergence story is completely different). It would be nice to know that exp and log are locally inverse to each other when defined on e.g. the p-adic numbers. Here the slick proof is to use real analytic methods to get the power series for exp and log, observe they're inverses on the reals, deduce that they're inverses as formal power series, and then deduce that they're inverses on the p-adics!

#### Mario Carneiro (Dec 16 2020 at 17:07):

In that case we should probably have a set of theorems that relate formal power series to real power series (or power series that converge in a more general topological group)

#### Ashvni Narayanan (Dec 16 2020 at 17:13):

Kevin Buzzard said:

I think that the formal power series identity will boil down to checking a fact about Bernouilli numbers which she already knows (because she showed me a proof last week), whereas checking the real identity will involve a whole lot of kerfuffle ultimately reducing to checking the formal power series identity. What do you think Ashvni? The definition of formal power series multiplication and the fact that two formal power series are equal iff they have the same coefficients should reduce you directly to something you know already, with the advantage that you can stay working over the rationals.

In the specific case of Bernoulli numbers and polynomials, I believe working with formal power series will be fine. I am more concerned with the proofs that will follow for p-adic L functions and zeta functions. As far as I can see, according to Washington, I think one can do with the formal power series identities.

#### Kevin Buzzard (Dec 16 2020 at 17:27):

Just as for the reals (and indeed the proof is even easier), when you're in a domain where your power series are converging, the sum/product as a function agrees with the sum/product as a power series. I think Mario is right -- one could imagine a cute little API here (probably one needs topological rings if one is dealing with power series, although it will boil down to topological groups at some point).

#### Ashvni Narayanan (Dec 16 2020 at 18:23):

I see, thank you! Maybe I could do it at some point in the future.

#### Kevin Buzzard (Dec 16 2020 at 19:45):

There is already an evaluation map from polynomials to rings, and I guess people spent some time figuring out how to set it up (I wasn't following it closely but there was `eval`

and `aeval`

and maybe even `eval_2`

or something). I guess the thing to do would be to see what decision people ultimately came to, and then set up the same system with $f\in R[[X]]$ and $t\in M$ where $M$ is a topological ring which is also an $R$-algebra; if the formal power series defining $f(t)$ is `summable`

then one can evaluate $f$ at $t$; one can then attempt to prove that if $f(t)$ and $g(t)$ are both summable then $(f+g)(t)=f(t)+g(t)$ and $(fg)(t)=f(t)g(t)$. These are the sorts of proofs which can sometimes be done in about 3 lines if you know the filter tricks I suspect.

#### Mario Carneiro (Dec 16 2020 at 20:03):

do we have the truncation map from a formal power series to a polynomial?

#### Mario Carneiro (Dec 16 2020 at 20:05):

That seems easier, and we will need lots of properties about it in order for the theory of formal series evaluation in a topological ring to go well, because it's basically the limit of that map as the truncation order tends to $\infty$

#### Heather Macbeth (Dec 16 2020 at 20:05):

I think part of the issue is making it work for multivariate polynomials and power series; this is what Yury's working on.

#### Johan Commelin (Dec 16 2020 at 20:06):

https://leanprover-community.github.io/mathlib_docs/ring_theory/power_series.html#power_series.trunc

#### Heather Macbeth (Dec 16 2020 at 20:07):

If I understand correctly there will be a map from docs#mv_power_series to docs#formal_multilinear_series

#### Mario Carneiro (Dec 16 2020 at 20:07):

oh, doing this mutivariate sounds like fun, there are so many ways to take the limit

#### Johan Commelin (Dec 16 2020 at 20:08):

right, that's why I only defined trunc in the single-variable case

#### Johan Commelin (Dec 16 2020 at 20:09):

it's not exactly clear what the right version for trunc would be in general

#### Heather Macbeth (Dec 16 2020 at 20:09):

and then the general theory, docs#formal_multilinear_series.le_radius_of_bound etc, will be used to construct the standard functions such as exp.

#### Mario Carneiro (Dec 16 2020 at 20:10):

you could throw it into `tsum`

, I suppose it will take the limit on the filter of monomials wrt inclusion, but it's not entirely clear to me if that's the limit you want (it's the "strongest" kind of limit you can ask for)

#### Mario Carneiro (Dec 16 2020 at 20:10):

it's equivalent to absolute convergence for functions on nat

#### Adam Topaz (Dec 16 2020 at 20:14):

Johan Commelin said:

it's not exactly clear what the right version for trunc would be in general

For power series the mathematically correct notion is the image of the power series in $A[X_1,\ldots,X_n]/(X_1,\ldots,X_n)^M$, i.e. you kill all monomials of total degree at least $M$. Laurent series is a different question altogether :)

#### Sebastien Gouezel (Dec 16 2020 at 20:15):

On the formal multilinear series side, this is docs#formal_multilinear_series.partial_sum

#### Adam Topaz (Dec 16 2020 at 20:17):

Oh, but `mv_powerseries`

can have infinitely many variables... oof

#### Mario Carneiro (Dec 16 2020 at 20:17):

This is good because that's exactly what `tsum`

does

#### Mario Carneiro (Dec 16 2020 at 20:17):

with infinitely many variables it takes the limit as you add more variables too

#### Adam Topaz (Dec 16 2020 at 20:19):

So algebraically this would be the limit of the mv_power_series rings over finitely many variables contained in the indexing set.

#### Mario Carneiro (Dec 16 2020 at 20:19):

of course that means that things like $X_1+X_2+\dots$ don't converge on $\Bbb R[[X_1,X_2,\dots]]$

#### Adam Topaz (Dec 16 2020 at 20:19):

I'm confused.

#### Mario Carneiro (Dec 16 2020 at 20:20):

Er, I mean the limit of that formal power series as mapped to $\Bbb R$ with $X_i\mapsto 1$ or something doesn't converge

#### Adam Topaz (Dec 16 2020 at 20:20):

Sure, you need to map to zero.

#### Mario Carneiro (Dec 16 2020 at 20:21):

If you map everything to 0 that's a kind of boring zeries

#### Mario Carneiro (Dec 16 2020 at 20:21):

unintentional pun

#### Mario Carneiro (Dec 16 2020 at 20:22):

If you map $X_i\mapsto 2^{-i}$ then it goes to 1 as you would expect

#### Adam Topaz (Dec 16 2020 at 20:23):

I guess I don't know what the definition of $\mathbb{R}[[X_1,X_2,\ldots]]$ is... (I mean algebraically)

#### Adam Topaz (Dec 16 2020 at 20:23):

Is it the completion w.r.t. the ideal $(X_1,X_2,\ldots)$?

#### Mario Carneiro (Dec 16 2020 at 20:23):

It is something like `multiset nat ->0 real`

#### Mario Carneiro (Dec 16 2020 at 20:24):

oh wait no `->0`

this isn't a polynomial

#### Mario Carneiro (Dec 16 2020 at 20:24):

it's just `multiset nat -> real`

#### Mario Carneiro (Dec 16 2020 at 20:25):

I don't understand your question/assertion. What is the ideal $(X_1, X_2, \dots)$?

#### Mario Carneiro (Dec 16 2020 at 20:25):

We need to construct the ring before we can do algebra on it

#### Adam Topaz (Dec 16 2020 at 20:26):

I mean take the polynomial ring $\mathbb{R}[X_1,X_2,\ldots]$, and take the completion of that w.r.t. $(X_1,X_2,\ldots)$.

#### Adam Topaz (Dec 16 2020 at 20:27):

That's one plausible definition of $\mathbb{R}[[X_1,X_2,\ldots]]$.

#### Mario Carneiro (Dec 16 2020 at 20:34):

I am no expert on these things, but that seems plausible based on the wikipedia definition. It's not obvious to me why the completion wouldn't have things like $X_1^\infty$ in it though

#### Riccardo Brasca (Dec 16 2020 at 21:16):

I think that $X_1 + X_2 + \cdots$ does not exist in $\mathbf{Z}[[X_1, X_2, \ldots]]$ (meaning that the series does not converge), if we define the latter as the completion of $\mathbf{Z}[X_1, X_2, \ldots]$ w.r.t. $(X_1, X_2, \ldots)$. The general term does not tend to $0$, right?

#### Kevin Buzzard (Dec 16 2020 at 21:24):

My instinct is to set up the one variable case, do the n variable case by induction on n and forget about the general case because I'm not sure it's useful

#### Mario Carneiro (Dec 16 2020 at 21:24):

noo

#### Mario Carneiro (Dec 16 2020 at 21:24):

induction on this kind of thing is painful

#### Mario Carneiro (Dec 16 2020 at 21:24):

index sets can usually be trivially finite or infinite

#### Kevin Buzzard (Dec 16 2020 at 21:25):

In which case my instinct is to stick to a fintype when doing evaluation

#### Kevin Buzzard (Dec 16 2020 at 21:25):

Because then there's no ambiguity

#### Mario Carneiro (Dec 16 2020 at 21:25):

I think the right thing will just happen automatically

#### Kevin Buzzard (Dec 16 2020 at 21:25):

I think that more than one thing can happen but I'm not sure I care about what happens in the infinite variable case

#### Mario Carneiro (Dec 16 2020 at 21:26):

then let's just do it and let what happens happen, and pretend that's what we wanted all along

#### Adam Topaz (Dec 16 2020 at 21:28):

The one natural place I know of where you have to consider expressions like $X_1 + X_2 + \cdots$ is when defining the ring of symmetric functions in countably many variables, which can be used to construct the ring of big Witt vectors. in this case you work with a subring of

$\lim_{n} \mathbb{Z}[X_1,\ldots,X_n]$

where the transition maps

$\mathbb{Z}[X_1,\ldots,X_{n+1}] \to \mathbb{Z}[X_1,\ldots,X_n]$

send $X_{n+1}$ to $0$.

#### Riccardo Brasca (Dec 16 2020 at 21:29):

It seems to me that an explicit description of $R[[X_0, X_2, \ldots]]$ is functions $f \colon \mathbf{N}^{(\mathbf{N})} \to R$ such that for all $d$ the set $\{ x \in \mathbf{N}^{(\mathbf{N})} \text{ such that } f(x) \neq 0 \text{ and } \sum_i x(i) = d \}$ is finite. In practice $x$ is just a finite sequence of natural numbers, giving a monomial (the exponents of $X_0,X_1,\ldots$ are given by the sequence) of (finite) degree $\sum_i x(i)$. Then a series exists if and only if it has only finitely many term of degree $d$, for any $d$.

#### Riccardo Brasca (Dec 16 2020 at 21:30):

Of course one can consider even bigger rings, but that's what we get taking completion w.r.t. $(X_1, X_2, \ldots)$

#### Kevin Buzzard (Dec 16 2020 at 21:33):

In Witt vectors I think you're working with a direct limit which is much smaller

#### Adam Topaz (Dec 16 2020 at 21:33):

No it's the inverse limit.

#### Adam Topaz (Dec 16 2020 at 21:34):

Well, it's the symmetric elements in that limit.

#### Kevin Buzzard (Dec 16 2020 at 21:34):

Aah you're right but it's the inverse limit of the polynomial rings not the power series rings

#### Adam Topaz (Dec 16 2020 at 21:34):

I like this reference for this approach: https://arxiv.org/pdf/math/0407227.pdf (see examples 2.10 and 3.2)

Last updated: May 17 2021 at 16:26 UTC