Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_AutomorphicForm_RankinSelbergQuotientIntegral.lean

definition module

Rankin–Selberg quotient integrand, quotient integral and shell-zero part

Throughout, K is a number field, and the adelic groups carry their Borel \sigma-algebras. Four definitions are made. First, quotientIntegrand takes carrier pins pins, an additive character \psi of \mathbb{A}_K, three complex-valued functions x,y,\varphi on \mathrm{GL}_2(\mathbb{A}_K), real parameters w,d_1,d_2, and a point g, and returns the product of five factors: the indicator (with value 1) of the set of g whose idele norm \lVert\det g\rVert, defined as the value of the distributive Haar character of \mathbb{A}_K at the idele \det g, lies in [d_1,d_2]; the Whittaker coefficient whittakerCoefficient K pins ψ x 1 g, i.e. \int \,x(u(t)g)\,\psi(-t)\,d\nu(t) over \mathbb{A}_K with respect to the measure carried by pins and with the character taken at the element 1\in K; the complex conjugate of the corresponding coefficient of y; the value \varphi(g); and the real scalar \lVert\det g\rVert^{-w} viewed in \mathbb{C}.

Second, quotientIntegral integrates this integrand over the orbit quotient RationalCentreUnipotentQuotient K of \mathrm{GL}_2(\mathbb{A}_K) by the subgroup generated by the rational central scalars and the adelic upper unipotents, with respect to the quotient measure built from Haar measure on \mathrm{GL}_2(\mathbb{A}_K) and the given measure on that subgroup; the integrand is evaluated at the chosen representative q.out of each class, so the definition is taken on a fixed choice of representatives rather than through an invariance statement. Third, shellZeroOutside S, for a finite set S of finite places, is the set of g such that at every v\notin S the valuation of the finite component of \det g at v equals \max(\lvert g_{10}\rvert_v,\lvert g_{11}\rvert_v)^2. Fourth, sPartIntegral is the same integral restricted to those classes whose chosen representative lies in shellZeroOutside K S.

Relation to Mathlib

Mathlib has no Rankin–Selberg integrals for adelic \mathrm{GL}_2; all four notions are the project's own, built on the project's adelic Haar measures, quotient-measure construction and Whittaker coefficients, with the idele norm taken from Mathlib's distribHaarChar.

Where it is used

These definitions provide the vocabulary in which the project states the unfolding of the Rankin–Selberg integral for \mathrm{GL}_2 over a number field and the separation of its Euler factors outside a finite set S of places, the shell-zero condition isolating the contribution of the places where the data are unramified.

References

  1. H. Jacquet, Automorphic Forms on GL(2), Part II, Lecture Notes in Mathematics 278, Springer, 1972
  2. D. Bump, Automorphic Forms and Representations, Cambridge Studies in Advanced Mathematics 55, Cambridge University Press, 1997, §3.8

References are suggested automatically and have not been individually verified.

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

Source file: Definitions/Def_AutomorphicForm_RankinSelbergQuotientIntegral.lean

Imports

Imported by

  • no other definition module

Declarations

Source

import Definitions.Def_AutomorphicForm_RationalCentreUnipotentQuotient
import Definitions.Def_AutomorphicForm_WhittakerCoefficient
import Definitions.Def_NumberField_TateGlobalZeta

open MeasureTheory NumberField NumberField.AdelicHaar NumberField.AdelicBox IsDedekindDomain

noncomputable section

namespace AutomorphicForm

namespace RankinSelberg

attribute [local instance] NumberField.AdelicHaar.glBorel NumberField.AdelicHaar.borelSpace_glBorel
  NumberField.AdelicHaar.adeleBorel NumberField.AdelicHaar.borelSpace_adeleBorel

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

def quotientIntegrand (pins : CarrierPins K) (ψ : AddChar (AdeleRing (𝓞 K) K) ℂ)
    (x y φ : AdelicGL2 (𝓞 K) K → ℂ) (w d₁ d₂ : ℝ) (g : AdelicGL2 (𝓞 K) K) : ℂ :=
  ({g : AdelicGL2 (𝓞 K) K |
        NumberField.TateGlobal.ideleNorm K (Matrix.GeneralLinearGroup.det g) ∈ Set.Icc d₁ d₂}.indicator
      (fun _ => (1 : ℂ)) g) *
    whittakerCoefficient K pins ψ x 1 g * (starRingEnd ℂ) (whittakerCoefficient K pins ψ y 1 g) * φ g *
    ((NumberField.TateGlobal.ideleNorm K (Matrix.GeneralLinearGroup.det g) ^ (-w) : ℝ) : ℂ)

def quotientIntegral (pins : CarrierPins K) (ψ : AddChar (AdeleRing (𝓞 K) K) ℂ)
    (x y φ : AdelicGL2 (𝓞 K) K → ℂ) (w d₁ d₂ : ℝ) : ℂ :=
  ∫ q : RationalCentreUnipotentQuotient K, quotientIntegrand K pins ψ x y φ w d₁ d₂ q.out
    ∂(rationalCentreUnipotentQuotientMeasure K)

def shellZeroOutside (S : Finset (HeightOneSpectrum (𝓞 K))) : Set (AdelicGL2 (𝓞 K) K) :=
  {g | ∀ v : HeightOneSpectrum (𝓞 K), v ∉ S →
    Valued.v ((((Matrix.GeneralLinearGroup.det g : (AdeleRing (𝓞 K) K)ˣ) : AdeleRing (𝓞 K) K)).2 v) =
      (max (Valued.v (((g : Matrix (Fin 2) (Fin 2) (AdeleRing (𝓞 K) K)) 1 0).2 v))
           (Valued.v (((g : Matrix (Fin 2) (Fin 2) (AdeleRing (𝓞 K) K)) 1 1).2 v))) ^ 2}

def sPartIntegral (S : Finset (HeightOneSpectrum (𝓞 K))) (pins : CarrierPins K)
    (ψ : AddChar (AdeleRing (𝓞 K) K) ℂ) (x y φ : AdelicGL2 (𝓞 K) K → ℂ) (w d₁ d₂ : ℝ) : ℂ :=
  ∫ q in {q : RationalCentreUnipotentQuotient K | q.out ∈ shellZeroOutside K S},
    quotientIntegrand K pins ψ x y φ w d₁ d₂ q.out ∂(rationalCentreUnipotentQuotientMeasure K)

end RankinSelberg

end AutomorphicForm

end

Statements phrased using this module (14)