Gonshor exponential

Stream: combinatorial-games

[Violeta Hernández]

How is the Gonshor exponential map $\exp$ defined? I haven't been able to find a simple and readable definition.

[Violeta Hernández]

Ok so after rereading Wikipedia enough I get it. The stuff with $[x]_{2n+1}$ is more convoluted than I would have liked, but I get it

[Aaron Liu]

Should we do what mathlib does and define a complex exponential first?

[Violeta Hernández]

Is the surcomplex exponential even a thing?

[Violeta Hernández]

Likely it is, but
a) If it generalizes from the Gonshor exponential then the generalization isn't trivial
b) I don't think this is anywhere in the literature

[Violeta Hernández]

I do really wish it exists, I wonder what stuff like cos(w) gives you

[Aaron Liu]

ah, going in circles is certainly a problem

[Aaron Liu]

Maybe you can take it mod 2pi i

[Violeta Hernández]

I wonder if there's some way to define surreal cosines and sines via Taylor series shenanigans that then gives an appropriate surcomplex exponential

[Violeta Hernández]

the Gonshor exponential feels like a hack though, you use not only the Taylor series expansion but the fact that exp(x+y) = exp(x) exp(y) and some monotonicity properties in order to define it

[Violeta Hernández]

if you can somehow do this with cosines it would be much worse

[Violeta Hernández]

Actually, fun fact: for an infinitesimal input, you can evaluate a real Taylor series on the surreals unambiguously

[Violeta Hernández]

... actually, wait

[Violeta Hernández]

Suppose S is a well-ordered subset of positive surreals. Denote by nS the pointwise sum of n copies of S. Conjecture: every surreal is in at most finitely many sets nS.

[Violeta Hernández]

(this implies that a real Taylor series on an infinitesimal input is well defined)

[Aaron Liu]

Violeta Hernández said:

I do really wish it exists, I wonder what stuff like cos(w) gives you

I think w is 2pi times an integer?

[Violeta Hernández]

Yes

[Violeta Hernández]

sort of? not really?

[Aaron Liu]

Does that mean 2pi is a rational number since w is also an integer

[Violeta Hernández]

if a surreal cosine existed I imagine it'd be

• the value of the Taylor series for infinitesimal or real inputs
• one for pure infinite inputs
• whatever the cosine addition formula tells you for a mix of both

[Violeta Hernández]

likewise for the sine

[Aaron Liu]

That sounds plausible I guess

[Aaron Liu]

does the Taylor series always give you a value?

[Violeta Hernández]

Wikipedia suggests that this is true for exp

[Aaron Liu]

How are you summing it up?

[Violeta Hernández]

Seems too good to be true for an arbitrary Taylor series and infinitesimal

[Violeta Hernández]

(deleted)

[Violeta Hernández]

Violeta Hernández said:

Suppose S is a well-ordered subset of positive surreals. Denote by nS the pointwise sum of n copies of S. Conjecture: every surreal is in at most finitely many sets nS.

You'd need this to be true, and also, for the union of all nS to be well-founded

[Violeta Hernández]

Aaron Liu said:

How are you summing it up?

Expand Conway forms, add like coefficients

[Aaron Liu]

How are you expanding powers of infinite sums?

[Aaron Liu]

Oh is that why you need the thing to be true

[Violeta Hernández]

That's just the definition of multiplication for Hahn series

[Aaron Liu]

wait you can multiply them

[Violeta Hernández]

the thing needs to be true so you can add like terms and join them into a new Hahn series

[Aaron Liu]

oh I think it's true

[Aaron Liu]

the thing is true

[Violeta Hernández]

oh, why?

[Violeta Hernández]

I'm completely stuck on this problem

[Violeta Hernández]

@Artie Khovanov Is this a known thing? "An infinitesimal Hahn series can be substituted into a real power series"

[Violeta Hernández]

Oh wait I'm really sorry, wrong person

[Violeta Hernández]

@Weiyi Wang

[Weiyi Wang]

(I was watchingthis thread just as I was mentioned :joy:)

[Weiyi Wang]

I think that is...true? If I understand what you mean correctly. By infintestimal, you mean the exponential of the leading term is positive, right

[Weiyi Wang]

wait...

[Violeta Hernández]

By infinitesimal I mean that the leading coefficient cx^r has r < 0, i.e. that the Hahn series is in a positive Archimedean class (assuming we haven't flipped the direction of those)

[Weiyi Wang]

I was using mathlib's definition where the leading term has the smallest r but I get your point

[Weiyi Wang]

I think you probably need the leading r to also not be infinitesimal to other r that appears in the series?

[Violeta Hernández]

To give an example, let z = x^-1 + x^-2 + ... Then you can formally substitute exp(z) = 1 + x^-1 + 3/2 x^-2 + 13/6 x^-3 + ...

The claim is that this works for any infinitesimal Hahn series z and any real Taylor series

[Weiyi Wang]

each power of the hahn series will raise its order. If this order tends to infinity, then we are good, as the coefficient of each term will be fixed after certain partial sum. If it doesn't tends to infinity, but eventually covers all terms we care about, then we are also fine, and we can set all other terms to 0

[Weiyi Wang]

if r is restricted to integers, this is fine, because it naturally goes to infinity

[Violeta Hernández]

What's the order? The largest exponent?

[Weiyi Wang]

yes (or the smallest in mathlib order)

[Weiyi Wang]

The case I am not sure about is when you have both ε and 1 in the exponent

[Aaron Liu]

Violeta Hernández said:

oh, why?

I realized my proof is wrong but surely it can be fixed

[Violeta Hernández]

If your exponents are all (negative) ordinals then the claim is simple to prove as well, any given ordinal must be the sum of no more other ordinals than the sum of its base w coefficients

[Violeta Hernández]

presumably the case where you have exponents in different Archimedean classes kind of behaves like this

[Aaron Liu]

Can we do some model theory magic to change the exponents into ordinals

[Violeta Hernández]

would be cool but i doubt it

[Violeta Hernández]

you can have very many exponents crammed into the same archimedean class

[Aaron Liu]

You can have many ordinals crammed into the same archimedean class

[Weiyi Wang]

How you evaluate a power series at (x^(-ε) + x^(-1+ε))? (following your convention that exponent goes downwards) The coefficient of x^(-1) feels undefined

[Weiyi Wang]

docs#HahnSeries.SummableFamily.powers is it true that we just need to change coefficients in this and we are good?

[Violeta Hernández]

Weiyi Wang said:

How you evaluate a power series at (x^(-ε) + x^(-1+ε))? (following your convention that exponent goes downwards) The coefficient of x^(-1) feels undefined

the only term that will contribute to that coefficient is the square :slight_smile:

[Violeta Hernández]

Weiyi Wang said:

docs#HahnSeries.SummableFamily.powers is it true that we just need to change coefficients in this and we are good?

Oh yeah! That's basically it

[Violeta Hernández]

Not at my computer rn, you happen to know what the proof idea is here?

[Weiyi Wang]

I am reading it for the first time

[Violeta Hernández]

From what I can gather, it's an application of Higman's lemma

[Violeta Hernández]

Which tracks, because this is the first time I ever read about Higman's lemma :sweat_smile:

[Violeta Hernández]

oh, it's a special case of Kruskal's tree theorem

[Violeta Hernández]

of TREE function fame

[Violeta Hernández]

Oh of course this is proved in Siegel as well
image.png

[Violeta Hernández]

Oh in fact you have an even stronger version
image.png

[Violeta Hernández]

Ok wow so apparently this is how you show that surreal numbers are real-closed

[Violeta Hernández]

I kinda expected that this would be some dark sorcery and not just applied Taylor series

[Violeta Hernández]

image.png
image.png
Screenshotting for posterity

[Artie Khovanov]

Looks like I guessed right and the proof for Puiseaux series generalises!

[Artie Khovanov]

I think we can state this argument very generally (it also works for lifting ACFs).

[Violeta Hernández]

I'm happy to announce Mathlib already has most Hahn series theory needed for this proof. We have docs#PowerSeries.heval, we're just missing the MvPowerSeries analog.