Exponential Fields & Transseries

Stream: Is there code for X?

[Antonio De Lucreziis]

It looks like there isn't anything from this branch of logic in mathlib:

https://en.wikipedia.org/wiki/Transseries

I was also looking for some docs on how one would start to formalize an object like this. More precisely, given a commutative ring $R$, i want to define the structure $(R, +, \times, <, \exp)$ in Lean. I tried writing an inductive type starting from a base ring $R$ and then adding exponential fields "operations" so $+$, $\times$ and $\exp$, but that only encodes "terms" of the structure and I loose all algebraic structure (i.e. I have to re-prove commutativity).

On the other hand, if I use the "type-class" approach I can easily define exponential fields in the axiomatic way, but then I lose the ability to match over term structure.

Is there an idiomatic way of doing this kind of things in Lean?

P.S. I don't know if this is the correct channel for this type of questions, in that case please tell me were I should move it

[Luigi Massacci]

What’s wrong with building on top of what is currently in mathlib’s model theory library?

[Luigi Massacci]

You can define that as a language expanding the language of rings (the latter being already there)

[Luigi Massacci]

There’s generic ordered structures but not ordered rings, but again you can combine the two (and add the appropriate compatibility axioms to the theory)

[Luigi Massacci]

see docs#FirstOrder.Language.ring

[Luigi Massacci]

The docs there also explain how to make this work alongside the standard Ring typeclass

[Luigi Massacci]

(the TLDR is: @Chris Hughes has already done the nasty part of setting this up for you, so you might as well reap the benefits instead of doing it from scratch)

[Chris Hughes]

I think the answer is different depending on what you want to do with this structure.

I think what it you actually want is to just define one particular type which is the type of formal transeries which is not a particularly easy type to define by the looks of it. You're best bet is to look at docs#HahnSeries and I suspect it's a special case of this by the looks of the wikipedia article (I don't know what a Transseries or a Hahn Series is so I'm not an expert here)

[Chris Hughes]

It's unlikely that anything to do with model theory is what you want. I wouldn't recommend using docs#FirstOrder.Language.ring

[Chris Hughes]

What you want is probably HahnSeries _ ℝ and I haven't quite figured out what goes in the placeholder for the _. It'll be some ordered abelian group, but I haven't quite worked out which one from the wikipedia article yet.

[Yaël Dillies]

Chris, I don't think this can be a Hahn series, since you can have a transseries as an exponent in another transseries

[Yaël Dillies]

You can however reuse docs#HahnSeries by following this construction: https://en.wikipedia.org/wiki/Transseries#Log-free_transseries

[Yaël Dillies]

The construction from surreal numbers might be the easiest one given the work we have on docs#Surreal: https://en.wikipedia.org/wiki/Transseries#Using_surreal_numbers

[Antonio De Lucreziis]

Thank you all. I already saw the Surreal numbers definition and I also think it is the one with the most similar construction. I'll let you know if me and my colleague make some progress on this!

[Violeta Hernández]

I've been thinking about this, precisely because of my work on surreal numbers. I do wonder if it's perhaps easier to define transseries as an iterated Hahn series construction, however. The fact that some subfield of the nimbers happens to be canonically isomorphic seems to me like more of a theorem than a definition.

[Violeta Hernández]

Moreover, it should be possible to characterize equality of transseries in a way that isn't dependent on the equality of surreal numbers.

[Violeta Hernández]

(Is there perhaps some notion of transseries built from fields other than ℝ? That would be another argument for not using Surreal in the definition)

[James E Hanson]

I think the general notion is that of a 'field of exponential-logarithmic series' over a given field. (See Appendix A of Aschenbrenner, van den Dries, and van der Hoeven.) It seems like the word 'transseries' is conventionally reserved specifically for $\mathbb{T} = \mathbb{R}((x^{-1}))^{\mathrm{LE}}$. (Although Aschenbrenner, van den Dries, and van der Hoeven mention that the terminology has been used differently in the literature.)

[Violeta Hernández]

Thanks for the reference! I was having trouble finding a transparent explanation for what transseries were.

[Violeta Hernández]

This all seems well within the grasp of Mathlib. A good starting project would be to define ExpTransSeries R Γ as the directed union starting with R⟦Γ⟧, according to the construction on pp. 611-612.

[Violeta Hernández]

I might try this in a few days if no one else does

[Violeta Hernández]

I'm starting work on this and I already ran into an issue. The linked paper gives a construction to extend a pre-exponential ordered field, and it describes taking a multiplicative copy exp(A) of an ordered additive group A, so to then define the field of Hahn series E⟦exp(A)⟧. The thing is, isn't the value group in a Hahn series supposed to be additive? HahnSeries.instField makes no mention of a multiplicative stucture on Γ.
image.png

[Weiyi Wang]

I think I have seen literature where HahnSeries' Γ is treated as a multiplicative group. Not sure if it is just a difference in convention here.

[Violeta Hernández]

Oh yeah, I think what they mean is that exp(A) is the multiplicative group of monomials.

[Violeta Hernández]

So the exponents themselves are still additive. Ah, mathematicians with their notation.

[Violeta Hernández]

Ok, I think I get it. Might as well give an example.

[Violeta Hernández]

Let's start with the field E₀ = ℝ⟦ℤ⟧ of Laurent series. We can "formally" take exponentials on elements of positive valuation (degree, order, whatever), and we can extend this to zero valuation by taking exp(r) equal to the standard real exponential. In order to take exponentials of elements with negative valuation, we create a new field E₁ = ℝ⟦ℤ⟧⟦ℝ⟦ℤ⟧^≺1⟧ ≃ ℝ⟦ℝ⟦ℤ⟧^≺1 ×ₗ ℤ⟧, so that exp(x) is identified with its monomial x for x ≺ 1. In this new field we can take exponentials of elements with non-negative valuation, and to address the remainder we create a new field E₂ = E₁⟦E₁^≺1⟧. And so on.

All of these fields Eₙ can be identified with Hahn series over ℝ. Their directed union (taken in the obvious way) will be the field of exponential transseries.

[Violeta Hernández]

I think a good first step might be to define a function HahnSeries.exp : ℝ⟦Γ⟧ → ℝ⟦Γ⟧. It'd be well-behaved on elements of non-negative valuation, and we could show that in this domain it is an additive character, strictly monotonic, and invertible. Then we could use this to "seed" the construction of transseries.

[Violeta Hernández]

Ok, so I've started writing code, and it turns out there's a lot of auxiliary definitions in the way of even having a definition of transseries. So here's my current design, at the moment only going as far to define exponential transseries.

Let Γ be a linearly ordered commutative (additive) group. We use mutual induction to define linearly ordered fields stepField Γ n and linearly ordered commutative groups stepGroup Γ n so that:

• stepField Γ 0 = ULift ℝ, stepGroup Γ 0 = Γ (the ULift is there for universe reasons)
• stepField Γ (n + 1) = Lex (stepField Γ n)⟦stepGroup Γ n⟧, stepGroup Γ (n + 1) = Lex (stepField Γ n)⟦{x : stepGroup Γ n // x < 0}⟧.

We also define the linearly ordered groups stepMonomial Γ n inductively, so that (there's gotta be a better way to do this):

• stepMonomial Γ 0 = Γ
• stepMonomial Γ (n + 1) = stepGroup Γ (n + 1) ×ₗ stepMonomial Γ n

Then, step Γ n = Lex (stepField Γ n)⟦stepGroup Γ n⟧ is the linearly ordered field of exponential transseries with exponential depth at most n, and we can prove it isomorphic to Lex ℝ⟦stepMonomial Γ n⟧.

Let monomial Γ be the direct limit of (the obvious system with) stepMonomial Γ n (again, there's probably a better way to do this). This direct system induces a direct system on Lex ℝ⟦stepMonomial Γ⟧, and its limit is ExpTransSeries Γ, which will embed (strictly) into Lex ℝ⟦monomial Γ⟧.

[Violeta Hernández]

Some questions:
a) Is this the correct definition?
b) Is there any better naming for all the definitions I've been prefixing with step?
c) Can the stuff with stepMonomial be simplified? (I don't think we currently have any sort of order instance on DirectSum, which is basically what I want).
d) Should these auxiliary definitions even be public API? Or should we just laser focus on defining transseries in their greatest generality?

[Violeta Hernández]

Also, sorry to be blunt, but is there anyone else interested/knowledgeable in this topic? Basically I'd like to know if I should use this topic to discuss my ideas or whether I should keep to my own until I have a PR ready. (Or is this too niche for Mathlib, even?)