Paris-Bonn

Stream: Geographic locality

[Bart Michels]

Hi, I'm a PhD student at Paris 13, but currently on an exchange in Bonn, working in analytic number theory and automorphic forms.

[Kevin Buzzard]

What definition of an automorphic form do you use? I have had my eye on the adelic definition for a while but there's still plenty of work to do before we have it.

[Bart Michels]

The classical one should be easier to implement, although it's not really the "right" definition. So you have semisimple Lie group G, the universal enveloping algebra U(g), a maximal compact subgroup K, discrete subgroup Gamma of finite co-volume (this last bit can be expressed without defining a measure on the quotient). U(g) has an action on smooth functions by its universal property (here you need vector fields, the Lie bracket), and take functions on G that are right K-invariant (say), left Gamma-invariant and that are joint eigenfunctions for the center Z(U(g)).
... and I forgot about Hecke operators, which are a pain unless G=SL_n and Gamma is very concrete, like SL_n(Z) or something that comes from a central simple algebra.

[Kevin Buzzard]

It seems to me that we're getting closer and closer to being able to state that definition in Lean. We have universal enveloping algebras but I'm not sure we have enough glue yet to enable them to act on functions on the Lie group.

[Bart Michels]

For analytic NT, I'm worried about things like:
log(1+O(x)) + (1+x)^2 = 1+O(x)
which are very common. (The example is very constructed of course, but O's do appear on both sides of the equality and sometimes nested. Equalities should always be read left-to-right with ∀ quantifiers over the O's in the LHS and ∃'s for the RHS.)
You can replace all O's by functions and formulate it as a ∀∃-statement about (partial) functions, but I'd like to approximate the notation we use as best as possible, even just as an experiment.

[Kevin Buzzard]

My impression is that the formalisation community only just started thinking seriously about O notation and I'm sure there's still a lot to learn.