Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_LanglandsTunnell_RSCarrier.lean

definition module

Rankin–Selberg local integral carriers for

For a group G equipped with a topology and a \sigma-algebra, RSCarrier.rsLocalIntegral takes a measure \mu on G, a subgroup H, a measure \mu_H on H, a function \delta : G \to \mathbb{R}, a complex parameter s and two functions W, F : G \to \mathbb{C}, and returns the Bochner integral of g \mapsto W(g)F(g)\,\delta(g)^{s-1/2} (the real value \delta(g) coerced into \mathbb{C} and raised to a complex power, with Mathlib's branch conventions) against \mu weighted by the density HaarQuotient.density H μH, i.e. the pointwise quotient of the \mathbb{R}_{\ge 0}^\infty-valued weight function attached to H and \mu_H by its \mu_H-average along left translates by H. The measures, the subgroup and the modulus \delta are data: no normalisation is fixed, and a non-integrable integrand yields 0.

Two instances are formed. Archimedean: RSCarrier.realUnipotent is the range of x \mapsto \begin{pmatrix}1&x\\0&1\end{pmatrix} in \mathrm{GL}_2(\mathbb{R}), and RSCarrier.rsArchIntegral is the above integral on \mathrm{GL}_2(\mathbb{R}) with \delta(g) = |\det g|. Finite: RSCarrier.finUnipotent is the adelic unipotent subgroup of \mathrm{GL}_2 over the adeles of \mathbb{Q}, viewed inside finiteAdelicGL2Subgroup ℚ (the kernel of the map to the archimedean components) via Subgroup.subgroupOf, and RSCarrier.rsFinIntegral is the integral on that subgroup with \delta(g) the idele norm of \det g, i.e. the real value of the distributive Haar character of the adele ring at \det g.

Two auxiliary definitions accompany the archimedean case: RSCarrier.transposeInv sends g \in \mathrm{GL}_2(\mathbb{R}) to (g^{-1})^{\mathsf T} (with inverse g^{\mathsf T}), and RSCarrier.archDual sends W to g \mapsto W\big(w\,(g^{-1})^{\mathsf T}\big), where w = \begin{pmatrix}0&1\\1&0\end{pmatrix} is the Weyl element AutomorphicForm.gl2Weyl.

Relation to Mathlib

Mathlib has Haar measures and measures on quotients, but no Rankin–Selberg integrals; both the integral and the weight/density construction used to build the integrating measure are the project's own.

Where it is used

These integrals form the analytic carrier for the Rankin–Selberg theory entering the Langlands–Tunnell theorem, which supplies the modularity of the mod 3 representation at the start of the Frey–Serre–Ribet–Wiles argument.

References

  1. H. Jacquet, I. I. Piatetski-Shapiro and J. A. Shalika, Rankin-Selberg convolutions, American Journal of Mathematics 105 (1983), 367–464
  2. J. Tunnell, Artin's conjecture for representations of octahedral type, Bulletin of the American Mathematical Society (N.S.) 5 (1981), 173–175
  3. 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.

Source file: Definitions/Def_LanglandsTunnell_RSCarrier.lean

Imports

Imported by

  • no other definition module

Declarations

Source

import Definitions.Def_AutomorphicForm_UnipotentQuotient
import Definitions.Def_AutomorphicForm_SmoothAutomorphicFnAt
import Definitions.Def_NumberField_TateGlobalZeta
import Definitions.Def_AutomorphicForm_WeylIntertwining

open MeasureTheory NumberField AutomorphicForm Matrix

noncomputable section

namespace RSCarrier

section Generic

variable {G : Type*} [Group G] [TopologicalSpace G] [MeasurableSpace G]

def rsLocalIntegral (μ : Measure G) (H : Subgroup G) (μH : Measure H) (δ : G → ℝ) (s : ℂ)
    (W F : G → ℂ) : ℂ :=
  ∫ g, (W g * F g) * ((δ g : ℝ) : ℂ) ^ (s - 1 / 2) ∂(μ.withDensity (HaarQuotient.density H μH))

end Generic

section Arch

abbrev realUnipotent : Subgroup (GL (Fin 2) ℝ) :=
  (unipotentGL2Hom (R := ℝ)).range

def rsArchIntegral [MeasurableSpace (GL (Fin 2) ℝ)] (μ : Measure (GL (Fin 2) ℝ))
    (μN : Measure realUnipotent) (s : ℂ) (W F : GL (Fin 2) ℝ → ℂ) : ℂ :=
  rsLocalIntegral μ realUnipotent μN (fun g => |(GeneralLinearGroup.det g : ℝ)|) s W F

def transposeInv (g : GL (Fin 2) ℝ) : GL (Fin 2) ℝ :=
  ⟨((g⁻¹ : GL (Fin 2) ℝ) : Matrix (Fin 2) (Fin 2) ℝ)ᵀ, (g : Matrix (Fin 2) (Fin 2) ℝ)ᵀ,
    by rw [← Matrix.transpose_mul]; simp,
    by rw [← Matrix.transpose_mul]; simp⟩

def archDual (W : GL (Fin 2) ℝ → ℂ) : GL (Fin 2) ℝ → ℂ :=
  fun g => W ((AutomorphicForm.gl2Weyl : GL (Fin 2) ℝ) * transposeInv g)

end Arch

section Finite

abbrev finUnipotent : Subgroup (finiteAdelicGL2Subgroup ℚ) :=
  (adelicUnipotent ℚ).subgroupOf (finiteAdelicGL2Subgroup ℚ)

def rsFinIntegral [MeasurableSpace (AdelicGL2 (𝓞 ℚ) ℚ)] (μ : Measure (finiteAdelicGL2Subgroup ℚ))
    (μN : Measure finUnipotent) (s : ℂ) (W F : finiteAdelicGL2Subgroup ℚ → ℂ) : ℂ :=
  rsLocalIntegral μ finUnipotent μN
    (fun g => TateGlobal.ideleNorm ℚ (GeneralLinearGroup.det (g : AdelicGL2 (𝓞 ℚ) ℚ))) s W F

end Finite

end RSCarrier

end

Statements phrased using this module (405)

… and 255 more statements (search for the module name to find them).