Documentation

Mathlib.NumberTheory.LSeries.AbstractFuncEq

Abstract functional equations for Mellin transforms #

This file formalises a general version of an argument used to prove functional equations for zeta and L functions.

FE-pairs #

We define a weak FE-pair to be a pair of functions f, g on the reals which are locally integrable on (0, ∞), have the form "constant" + "rapidly decaying term" at , and satisfy a functional equation of the form

f (1 / x) = ε * x ^ k * g x

for some constants k ∈ ℝ and ε ∈ ℂ. (Modular forms give rise to natural examples with k being the weight and ε the global root number; hence the notation.) We could arrange ε = 1 by scaling g; but this is inconvenient in applications so we set things up more generally.

A strong FE-pair is a weak FE-pair where the constant terms of f and g at are both 0.

The main property of these pairs is the following: if f, g are a weak FE-pair, with constant terms f₀ and g₀ at , then the Mellin transforms Λ and Λ' of f - f₀ and g - g₀ respectively both have meromorphic continuation and satisfy a functional equation of the form

Λ (k - s) = ε * Λ' s.

The poles (and their residues) are explicitly given in terms of f₀ and g₀; in particular, if (f, g) are a strong FE-pair, then the Mellin transforms of f and g are entire functions.

Main definitions and results #

See the sections Main theorems on weak FE-pairs and Main theorems on strong FE-pairs below.

Definitions and symmetry #

structure WeakFEPair (E : Type u_1) [NormedAddCommGroup E] [NormedSpace E] :
Type u_1

A structure designed to hold the hypotheses for the Mellin-functional-equation argument (most general version: rapid decay at up to constant terms)

  • f : E

    The functions whose Mellin transform we study

  • g : E

    The functions whose Mellin transform we study

  • k :

    Weight (exponent in the functional equation)

  • ε :

    Root number

  • f₀ : E

    Constant terms at

  • g₀ : E

    Constant terms at

  • hf_int : MeasureTheory.LocallyIntegrableOn self.f (Set.Ioi 0) MeasureTheory.volume
  • hg_int : MeasureTheory.LocallyIntegrableOn self.g (Set.Ioi 0) MeasureTheory.volume
  • hk : 0 < self.k
  • hε : self 0
  • h_feq : xSet.Ioi 0, self.f (1 / x) = (self * (x ^ self.k)) self.g x
  • hf_top : ∀ (r : ), (fun (x : ) => self.f x - self.f₀) =O[Filter.atTop] fun (x : ) => x ^ r
  • hg_top : ∀ (r : ), (fun (x : ) => self.g x - self.g₀) =O[Filter.atTop] fun (x : ) => x ^ r
theorem WeakFEPair.hf_int {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (self : WeakFEPair E) :
MeasureTheory.LocallyIntegrableOn self.f (Set.Ioi 0) MeasureTheory.volume
theorem WeakFEPair.hg_int {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (self : WeakFEPair E) :
MeasureTheory.LocallyIntegrableOn self.g (Set.Ioi 0) MeasureTheory.volume
theorem WeakFEPair.hk {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (self : WeakFEPair E) :
0 < self.k
theorem WeakFEPair. {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (self : WeakFEPair E) :
self 0
theorem WeakFEPair.h_feq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (self : WeakFEPair E) (x : ) :
x Set.Ioi 0self.f (1 / x) = (self * (x ^ self.k)) self.g x
theorem WeakFEPair.hf_top {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (self : WeakFEPair E) (r : ) :
(fun (x : ) => self.f x - self.f₀) =O[Filter.atTop] fun (x : ) => x ^ r
theorem WeakFEPair.hg_top {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (self : WeakFEPair E) (r : ) :
(fun (x : ) => self.g x - self.g₀) =O[Filter.atTop] fun (x : ) => x ^ r
structure StrongFEPair (E : Type u_1) [NormedAddCommGroup E] [NormedSpace E] extends WeakFEPair :
Type u_1

A structure designed to hold the hypotheses for the Mellin-functional-equation argument (version without constant terms)

theorem StrongFEPair.hf₀ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (self : StrongFEPair E) :
self.f₀ = 0
theorem StrongFEPair.hg₀ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (self : StrongFEPair E) :
self.g₀ = 0
theorem WeakFEPair.h_feq' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (P : WeakFEPair E) (x : ) (hx : 0 < x) :
P.g (1 / x) = (P⁻¹ * (x ^ P.k)) P.f x

Reformulated functional equation with f and g interchanged.

The hypotheses are symmetric in f and g, with the constant ε replaced by ε⁻¹.

Equations
  • P.symm = { f := P.g, g := P.f, k := P.k, ε := P⁻¹, f₀ := P.g₀, g₀ := P.f₀, hf_int := , hg_int := , hk := , := , h_feq := , hf_top := , hg_top := }

The hypotheses are symmetric in f and g, with the constant ε replaced by ε⁻¹.

Equations
  • P.symm = { toWeakFEPair := P.symm, hf₀ := , hg₀ := }

Auxiliary results I: lemmas on asymptotics #

theorem WeakFEPair.hf_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (P : WeakFEPair E) (r : ) :
(fun (x : ) => P.f x - (P * (x ^ (-P.k))) P.g₀) =O[nhdsWithin 0 (Set.Ioi 0)] fun (x : ) => x ^ r

As x → 0, we have f x = x ^ (-P.k) • constant up to a rapidly decaying error.

theorem WeakFEPair.hf_zero' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (P : WeakFEPair E) :
(fun (x : ) => P.f x - P.f₀) =O[nhdsWithin 0 (Set.Ioi 0)] fun (x : ) => x ^ (-P.k)

Power asymptotic for f - f₀ as x → 0.

theorem StrongFEPair.hf_top' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (P : StrongFEPair E) (r : ) :
P.f =O[Filter.atTop] fun (x : ) => x ^ r

As x → ∞, f x decays faster than any power of x.

theorem StrongFEPair.hf_zero' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (P : StrongFEPair E) (r : ) :
P.f =O[nhdsWithin 0 (Set.Ioi 0)] fun (x : ) => x ^ r

As x → 0, f x decays faster than any power of x.

Main theorems on strong FE-pairs #

The completed L-function.

Equations
theorem StrongFEPair.hasMellin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (P : StrongFEPair E) (s : ) :
HasMellin P.f s (P s)

The Mellin transform of f is well-defined and equal to P.Λ s, for all s.

theorem StrongFEPair.symm_Λ_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (P : StrongFEPair E) :
P.symm = mellin P.g

If (f, g) are a strong FE pair, then the Mellin transform of f is entire.

theorem StrongFEPair.functional_equation {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (P : StrongFEPair E) (s : ) :
P (P.k - s) = P P.symm s

Main theorem about strong FE pairs: if (f, g) are a strong FE pair, then the Mellin transforms of f and g are related by s ↦ k - s.

This is proved by making a substitution t ↦ t⁻¹ in the Mellin transform integral.

Auxiliary results II: building a strong FE-pair from a weak FE-pair #

Piecewise modified version of f with optimal asymptotics. We deliberately choose intervals which don't quite join up, so the function is 0 at x = 1, in order to maintain symmetry; there is no "good" choice of value at 1.

Equations
  • P.f_modif = ((Set.Ioi 1).indicator fun (x : ) => P.f x - P.f₀) + (Set.Ioo 0 1).indicator fun (x : ) => P.f x - (P * (x ^ (-P.k))) P.g₀

Piecewise modified version of g with optimal asymptotics.

Equations
theorem WeakFEPair.hf_modif_int {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (P : WeakFEPair E) :
MeasureTheory.LocallyIntegrableOn P.f_modif (Set.Ioi 0) MeasureTheory.volume
theorem WeakFEPair.hf_modif_FE {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (P : WeakFEPair E) (x : ) (hx : 0 < x) :
P.f_modif (1 / x) = (P * (x ^ P.k)) P.g_modif x

Given a weak FE-pair (f, g), modify it into a strong FE-pair by subtracting suitable correction terms from f and g.

Equations
  • One or more equations did not get rendered due to their size.
theorem WeakFEPair.f_modif_aux1 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (P : WeakFEPair E) :
Set.EqOn (fun (x : ) => P.f_modif x - P.f x + P.f₀) (((Set.Ioo 0 1).indicator fun (x : ) => P.f₀ - (P * (x ^ (-P.k))) P.g₀) + {1}.indicator fun (x : ) => P.f₀ - P.f 1) (Set.Ioi 0)
theorem WeakFEPair.f_modif_aux2 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (P : WeakFEPair E) [CompleteSpace E] {s : } (hs : P.k < s.re) :
mellin (fun (x : ) => P.f_modif x - P.f x + P.f₀) s = (1 / s) P.f₀ + (P / (P.k - s)) P.g₀

Compute the Mellin transform of the modifying term used to kill off the constants at 0 and .

Main theorems on weak FE-pairs #

An entire function which differs from the Mellin transform of f - f₀, where defined, by a correction term of the form A / s + B / (k - s).

Equations
def WeakFEPair.Λ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (P : WeakFEPair E) (s : ) :
E

A meromorphic function which agrees with the Mellin transform of f - f₀ where defined

Equations
  • P s = P.Λ₀ s - (1 / s) P.f₀ - (P / (P.k - s)) P.g₀
theorem WeakFEPair.Λ₀_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (P : WeakFEPair E) (s : ) :
P.Λ₀ s = P s + (1 / s) P.f₀ + (P / (P.k - s)) P.g₀
theorem WeakFEPair.symm_Λ₀_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (P : WeakFEPair E) (s : ) :
P.symm.Λ₀ s = P.symm s + (1 / s) P.g₀ + (P⁻¹ / (P.k - s)) P.f₀
theorem WeakFEPair.differentiableAt_Λ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (P : WeakFEPair E) {s : } (hs : s 0 P.f₀ = 0) (hs' : s P.k P.g₀ = 0) :
theorem WeakFEPair.hasMellin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (P : WeakFEPair E) [CompleteSpace E] {s : } (hs : P.k < s.re) :
HasMellin (fun (x : ) => P.f x - P.f₀) s (P s)

Relation between Λ s and the Mellin transform of f - f₀, where the latter is defined.

theorem WeakFEPair.functional_equation₀ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (P : WeakFEPair E) (s : ) :
P.Λ₀ (P.k - s) = P P.symm.Λ₀ s

Functional equation formulated for Λ₀.

theorem WeakFEPair.functional_equation {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (P : WeakFEPair E) (s : ) :
P (P.k - s) = P P.symm s

Functional equation formulated for Λ.

theorem WeakFEPair.Λ_residue_k {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (P : WeakFEPair E) :
Filter.Tendsto (fun (s : ) => (s - P.k) P s) (nhdsWithin P.k {P.k}) (nhds (P P.g₀))

The residue of Λ at s = k is equal to εg₀.

theorem WeakFEPair.Λ_residue_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (P : WeakFEPair E) :
Filter.Tendsto (fun (s : ) => s P s) (nhdsWithin 0 {0}) (nhds (-P.f₀))

The residue of Λ at s = 0 is equal to -f₀.