`Definitions/Def_AutomorphicForm_PeterssonIntegral.lean`

definition module

Weighted Petersson integral on adelic GL(2)

For a number field F this module defines a single object, AutomorphicForm.peterssonIntegral. Its data are a real exponent s, a set S \subseteq \mathrm{GL}_2(\mathbb{A}_F) (where \mathrm{GL}_2(\mathbb{A}_F) is the project's AdelicGL2 = \mathrm{GL}_2 of the adele ring of F) and two functions x, y \colon \mathrm{GL}_2(\mathbb{A}_F) \to \mathbb{C}; its value is the complex number \int_S x(g)\,\overline{y(g)}\;\bigl(\,\|\det g\|^{-s}\bigr)\,dg, the integral being a Bochner integral over S against the Haar measure adelicGLHaar (Fin 2) (𝓞 F) F for the Borel \sigma-algebra glBorel (Fin 2) (𝓞 F) F (this measurable-space instance is installed inside the definition by letI). Here \overline{\phantom{y}} is complex conjugation (starRingEnd ℂ), \det g is taken as a unit of \mathbb{A}_F, and \|\cdot\| is the project's NumberField.TateGlobal.ideleNorm, defined as the value of Mathlib's module-Haar character distribHaarChar of the adele ring on the given idele, viewed as a positive real; the real power \|\det g\|^{-s} is then coerced into \mathbb{C}.

This is a plain definition: no integrability hypothesis is imposed, so for non-integrable integrands the value is 0 by the convention governing the Bochner integral, and no invariance, positivity or independence of S is asserted. The pairing is linear in x and conjugate-linear in y; with s the integral is twisted by \|\det g\|^{-s}, which for s = 0 gives the unweighted Petersson integral over S.

Relation to Mathlib

Mathlib has no Petersson pairing for automorphic functions on adelic \mathrm{GL}_2; this is the project's own definition. It is built from Mathlib's Bochner integral and from the project's Haar measure adelicGLHaar (Mathlib's Measure.haar for the Borel structure on \mathrm{GL}_2 of the adeles) and idele norm ideleNorm (Mathlib's distribHaarChar of the adele ring).

Where it is used

The weighted Petersson integral provides the inner product used on the analytic side of the modularity argument, where automorphic forms on \mathrm{GL}_2(\mathbb{A}_F) are treated as square-integrable functions on a region S of the adelic group, the factor \|\det g\|^{-s} absorbing a central character.

References

D. Bump, Automorphic Forms and Representations, Cambridge Studies in Advanced Mathematics 55, Cambridge University Press, 1997
S. Gelbart, Automorphic Forms on Adele Groups, Annals of Mathematics Studies 83, Princeton University Press, 1975
H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

23 lines
1 declarations
used in the statements of 20 theorems and imported by 39 proofs
imports 1 definition modules

Source file: Definitions/Def_AutomorphicForm_PeterssonIntegral.lean

Imports

Def_NumberField_TateGlobalZeta

Imported by

no other definition module

Declarations

defAutomorphicForm.peterssonIntegral

Source

import Definitions.Def_NumberField_TateGlobalZeta

set_option autoImplicit false

noncomputable section

open NumberField NumberField.AdelicHaar

namespace AutomorphicForm

variable (F : Type) [Field F] [NumberField F]

def peterssonIntegral (s : ℝ) (S : Set (AdelicGL2 (𝓞 F) F)) (x y : AdelicGL2 (𝓞 F) F → ℂ) : ℂ :=
  letI := glBorel (Fin 2) (𝓞 F) F
  ∫ g in S,
    x g * (starRingEnd ℂ) (y g) *
      ((NumberField.TateGlobal.ideleNorm F (Matrix.GeneralLinearGroup.det g) ^ (-s) : ℝ) : ℂ)
    ∂(adelicGLHaar (Fin 2) (𝓞 F) F)

end AutomorphicForm

end

Definitions/Def_AutomorphicForm_PeterssonIntegral.lean