Zulip Chat Archive

Stream: Is there code for X?

Topic: Exponential


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

view this post on Zulip Eric Wieser (Dec 16 2020 at 16:24):

Perhaps something near src#complex.exp'?

view this post on Zulip Kevin Buzzard (Dec 16 2020 at 16:25):

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

view this post on Zulip Ashvni Narayanan (Dec 16 2020 at 16:28):

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

view this post on Zulip Johan Commelin (Dec 16 2020 at 16:28):

No, exp is the function, not the number

view this post on Zulip Johan Commelin (Dec 16 2020 at 16:29):

real.exp x =ex= e^x

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

view this post on Zulip Heather Macbeth (Dec 16 2020 at 16:30):

Why do you need it?

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

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

view this post on Zulip Kevin Buzzard (Dec 16 2020 at 16:33):

We have formal power series in Lean

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

view this post on Zulip Kevin Buzzard (Dec 16 2020 at 16:55):

Indeed I do :-)

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

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

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

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

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

view this post on Zulip Ashvni Narayanan (Dec 16 2020 at 18:23):

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

view this post on Zulip 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 fR[[X]]f\in R[[X]] and tMt\in M where MM is a topological ring which is also an RR-algebra; if the formal power series defining f(t)f(t) is summable then one can evaluate ff at tt; one can then attempt to prove that if f(t)f(t) and g(t)g(t) are both summable then (f+g)(t)=f(t)+g(t)(f+g)(t)=f(t)+g(t) and (fg)(t)=f(t)g(t)(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.

view this post on Zulip Mario Carneiro (Dec 16 2020 at 20:03):

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

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

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

view this post on Zulip Johan Commelin (Dec 16 2020 at 20:06):

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

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

view this post on Zulip Mario Carneiro (Dec 16 2020 at 20:07):

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

view this post on Zulip Johan Commelin (Dec 16 2020 at 20:08):

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

view this post on Zulip Johan Commelin (Dec 16 2020 at 20:09):

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

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

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

view this post on Zulip Mario Carneiro (Dec 16 2020 at 20:10):

it's equivalent to absolute convergence for functions on nat

view this post on Zulip 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[X1,,Xn]/(X1,,Xn)MA[X_1,\ldots,X_n]/(X_1,\ldots,X_n)^M, i.e. you kill all monomials of total degree at least MM. Laurent series is a different question altogether :)

view this post on Zulip Sebastien Gouezel (Dec 16 2020 at 20:15):

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

view this post on Zulip Adam Topaz (Dec 16 2020 at 20:17):

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

view this post on Zulip Mario Carneiro (Dec 16 2020 at 20:17):

This is good because that's exactly what tsum does

view this post on Zulip Mario Carneiro (Dec 16 2020 at 20:17):

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

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

view this post on Zulip Mario Carneiro (Dec 16 2020 at 20:19):

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

view this post on Zulip Adam Topaz (Dec 16 2020 at 20:19):

I'm confused.

view this post on Zulip Mario Carneiro (Dec 16 2020 at 20:20):

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

view this post on Zulip Adam Topaz (Dec 16 2020 at 20:20):

Sure, you need to map to zero.

view this post on Zulip Mario Carneiro (Dec 16 2020 at 20:21):

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

view this post on Zulip Mario Carneiro (Dec 16 2020 at 20:21):

unintentional pun

view this post on Zulip Mario Carneiro (Dec 16 2020 at 20:22):

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

view this post on Zulip Adam Topaz (Dec 16 2020 at 20:23):

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

view this post on Zulip Adam Topaz (Dec 16 2020 at 20:23):

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

view this post on Zulip Mario Carneiro (Dec 16 2020 at 20:23):

It is something like multiset nat ->0 real

view this post on Zulip Mario Carneiro (Dec 16 2020 at 20:24):

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

view this post on Zulip Mario Carneiro (Dec 16 2020 at 20:24):

it's just multiset nat -> real

view this post on Zulip Mario Carneiro (Dec 16 2020 at 20:25):

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

view this post on Zulip Mario Carneiro (Dec 16 2020 at 20:25):

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

view this post on Zulip Adam Topaz (Dec 16 2020 at 20:26):

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

view this post on Zulip Adam Topaz (Dec 16 2020 at 20:27):

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

view this post on Zulip 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 X1X_1^\infty in it though

view this post on Zulip Riccardo Brasca (Dec 16 2020 at 21:16):

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

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

view this post on Zulip Mario Carneiro (Dec 16 2020 at 21:24):

noo

view this post on Zulip Mario Carneiro (Dec 16 2020 at 21:24):

induction on this kind of thing is painful

view this post on Zulip Mario Carneiro (Dec 16 2020 at 21:24):

index sets can usually be trivially finite or infinite

view this post on Zulip Kevin Buzzard (Dec 16 2020 at 21:25):

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

view this post on Zulip Kevin Buzzard (Dec 16 2020 at 21:25):

Because then there's no ambiguity

view this post on Zulip Mario Carneiro (Dec 16 2020 at 21:25):

I think the right thing will just happen automatically

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

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

view this post on Zulip Adam Topaz (Dec 16 2020 at 21:28):

The one natural place I know of where you have to consider expressions like X1+X2+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

limnZ[X1,,Xn]\lim_{n} \mathbb{Z}[X_1,\ldots,X_n]

where the transition maps

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

send Xn+1X_{n+1} to 00.

view this post on Zulip Riccardo Brasca (Dec 16 2020 at 21:29):

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

view this post on Zulip 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. (X1,X2,)(X_1, X_2, \ldots)

view this post on Zulip Kevin Buzzard (Dec 16 2020 at 21:33):

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

view this post on Zulip Adam Topaz (Dec 16 2020 at 21:33):

No it's the inverse limit.

view this post on Zulip Adam Topaz (Dec 16 2020 at 21:34):

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

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

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