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
Instances For
    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)

    Instances For
      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 := }
      Instances For

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

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

          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
          Instances For
            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₀
            Instances For

              Piecewise modified version of g with optimal asymptotics.

              Equations
              Instances For
                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.
                Instances For
                  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
                  Instances For
                    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₀
                    Instances For
                      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₀.