Exponential

Stream: Is there code for X?

[Ashvni Narayanan]

Is there a file which describes real.exp^x as a tsum or sum?

Any help is appreciated, thank you!

[Eric Wieser]

Perhaps something near src#complex.exp'?

[Kevin Buzzard]

What do you mean by real.exp^x? Do you just mean real.exp?

[Ashvni Narayanan]

Yes, sorry, I mean the Taylor series corresponding to e^x where e is real.exp

[Johan Commelin]

No, exp is the function, not the number

[Johan Commelin]

real.exp x $= e^x$

[Heather Macbeth]

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

[Heather Macbeth]

Why do you need it?

[Ashvni Narayanan]

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]

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

[Kevin Buzzard]

We have formal power series in Lean

[Heather Macbeth]

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]

Indeed I do :-)

[Kevin Buzzard]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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]

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]

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

[Heather Macbeth]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Heather Macbeth]

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]

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]

it's equivalent to absolute convergence for functions on nat

[Adam Topaz]

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]

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

[Adam Topaz]

Oh, but mv_powerseries can have infinitely many variables... oof

[Mario Carneiro]

This is good because that's exactly what tsum does

[Mario Carneiro]

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

[Adam Topaz]

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

[Mario Carneiro]

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]

I'm confused.

[Mario Carneiro]

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]

Sure, you need to map to zero.

[Mario Carneiro]

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

[Mario Carneiro]

unintentional pun

[Mario Carneiro]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Mario Carneiro]

It is something like multiset nat ->0 real

[Mario Carneiro]

oh wait no ->0 this isn't a polynomial

[Mario Carneiro]

it's just multiset nat -> real

[Mario Carneiro]

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

[Mario Carneiro]

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

[Adam Topaz]

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]

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

[Mario Carneiro]

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]

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]

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]

noo

[Mario Carneiro]

induction on this kind of thing is painful

[Mario Carneiro]

index sets can usually be trivially finite or infinite

[Kevin Buzzard]

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

[Kevin Buzzard]

Because then there's no ambiguity

[Mario Carneiro]

I think the right thing will just happen automatically

[Kevin Buzzard]

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]

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

[Adam Topaz]

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]

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]

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]

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

[Adam Topaz]

No it's the inverse limit.

[Adam Topaz]

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

[Kevin Buzzard]

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

[Adam Topaz]

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