Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_AutomorphicForm_RightConvolution.lean

definition module

Right convolution of complex functions on adelic

Fix a number field K, with ring of integers \mathcal{O}_K and adele ring \mathbb{A}_K, and consider the locally compact group G = \mathrm{GL}_2(\mathbb{A}_K), equipped with its Borel \sigma-algebra (AdelicHaar.glBorel) and the left Haar measure AdelicHaar.adelicGLHaar, which is Mathlib's Measure.haar for this group and Borel structure. For two arbitrary functions \varphi, f \colon G \to \mathbb{C}, AutomorphicForm.rightConv is the function (\varphi * f)(g) \;=\; \int_G \varphi(gx)\, f(x)\, dx , the integral being the Bochner integral against that Haar measure; by the usual convention it takes the value 0 at any g for which x \mapsto \varphi(gx)f(x) fails to be integrable. No measurability, integrability, continuity, support or invariance condition is imposed on \varphi or f: the definition is total on pairs of set-theoretic functions, and rightConv_apply simply restates the defining formula.

Three elementary properties accompany the definition. rightConv_zero_right and rightConv_zero_left state that \varphi * f is the zero function as soon as f or \varphi is the zero function. rightConv_comp_mul_left states the compatibility with left translation in the first argument: for h, g \in G, the right convolution of x \mapsto \varphi(hx) with f, evaluated at g, equals (\varphi * f)(hg); this rests only on associativity of multiplication in G and not on any invariance property of the measure. Thus \varphi \mapsto \varphi * f is the operator \int_G f(x)\,\rho(x)\,dx built from the right-translation action \rho, and the recorded lemma says precisely that it commutes with left translations.

Relation to Mathlib

Mathlib's MeasureTheory.convolution is formulated for convolution on additive groups; the operator here is defined directly as an integral over \mathrm{GL}_2(\mathbb{A}_K) against the Haar measure AdelicHaar.adelicGLHaar of the project's adelic measure-theory module, which itself specialises Mathlib's Measure.haar to this group.

Where it is used

The intended use is as the smoothing operator of the theory of automorphic forms: taking f a test function on \mathrm{GL}_2(\mathbb{A}_K), the map \varphi \mapsto \varphi * f regularises a function on the adelic group while, by the translation property recorded here, preserving left invariance under a subgroup.

References

  1. D. Bump, Automorphic Forms and Representations, Cambridge Studies in Advanced Mathematics 55, Cambridge University Press, 1997
  2. S. Gelbart, Automorphic Forms on Adèle Groups, Annals of Mathematics Studies 83, Princeton University Press, 1975

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_RightConvolution.lean

Imports

Imported by

Declarations

Source

import Definitions.Def_NumberField_AdelicHaar

open NumberField

namespace AutomorphicForm

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

noncomputable def rightConv (φ f : GL (Fin 2) (AdeleRing (𝓞 K) K) → ℂ) :
    GL (Fin 2) (AdeleRing (𝓞 K) K) → ℂ :=
  fun g =>
    (letI := AdelicHaar.glBorel (Fin 2) (𝓞 K) K
     ∫ x, φ (g * x) * f x ∂(AdelicHaar.adelicGLHaar (Fin 2) (𝓞 K) K))

theorem rightConv_apply (φ f : GL (Fin 2) (AdeleRing (𝓞 K) K) → ℂ)
    (g : GL (Fin 2) (AdeleRing (𝓞 K) K)) :
    rightConv K φ f g =
      (letI := AdelicHaar.glBorel (Fin 2) (𝓞 K) K
       ∫ x, φ (g * x) * f x ∂(AdelicHaar.adelicGLHaar (Fin 2) (𝓞 K) K)) :=
  rfl

theorem rightConv_zero_right (φ : GL (Fin 2) (AdeleRing (𝓞 K) K) → ℂ) :
    rightConv K φ (fun _ => 0) = fun _ => 0 := by
  funext g
  simp [rightConv]

theorem rightConv_zero_left (f : GL (Fin 2) (AdeleRing (𝓞 K) K) → ℂ) :
    rightConv K (fun _ => 0) f = fun _ => 0 := by
  funext g
  simp [rightConv]

theorem rightConv_comp_mul_left (φ f : GL (Fin 2) (AdeleRing (𝓞 K) K) → ℂ)
    (h g : GL (Fin 2) (AdeleRing (𝓞 K) K)) :
    rightConv K (fun x => φ (h * x)) f g = rightConv K φ f (h * g) := by
  simp only [rightConv, mul_assoc]

end AutomorphicForm

Statements phrased using this module (356)

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