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.

• Strong FE pairs:
  • StrongFEPair.Λ : function of s : ℂ
  • StrongFEPair.differentiable_Λ: Λ is entire
  • StrongFEPair.hasMellin: Λ is everywhere equal to the Mellin transform of f
  • StrongFEPair.functional_equation: the functional equation for Λ
• Weak FE pairs:
  • WeakFEPair.Λ₀: and WeakFEPair.Λ: functions of s : ℂ
  • WeakFEPair.differentiable_Λ₀: Λ₀ is entire
  • WeakFEPair.differentiableAt_Λ: Λ is differentiable away from s = 0 and s = k
  • WeakFEPair.hasMellin: for k < re s, Λ s equals the Mellin transform of f - f₀
  • WeakFEPair.functional_equation₀: the functional equation for Λ₀
  • WeakFEPair.functional_equation: the functional equation for Λ
  • WeakFEPair.Λ_residue_k: computation of the residue at k
  • WeakFEPair.Λ_residue_zero: computation of the residue at 0.

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 : ∀ x ∈ Set.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.hε {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 0 → self.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)

• f : ℝ → E
• g : ℝ → E
• k : ℝ
• ε : ℂ
• f₀ : E
• g₀ : E
• 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 : ∀ x ∈ Set.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
• hf₀ : self.f₀ = 0
• hg₀ : self.g₀ = 0

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.

def WeakFEPair.symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (P : WeakFEPair E) : WeakFEPair E

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ε := ⋯, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ }

def StrongFEPair.symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (P : StrongFEPair E) : StrongFEPair E

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

def StrongFEPair.Λ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (P : StrongFEPair E) : ℂ → E

The completed L-function.

Equations

• P.Λ = mellin P.f

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.Λ_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (P : StrongFEPair E) : P.Λ = mellin P.f

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

theorem StrongFEPair.differentiable_Λ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (P : StrongFEPair E) : Differentiable ℂ P.Λ

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

def WeakFEPair.f_modif {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (P : WeakFEPair E) : ℝ → E

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₀

def WeakFEPair.g_modif {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (P : WeakFEPair E) : ℝ → E

Piecewise modified version of g with optimal asymptotics.

Equations

• P.g_modif = ((Set.Ioi 1).indicator fun (x : ℝ) => P.g x - P.g₀) + (Set.Ioo 0 1).indicator fun (x : ℝ) => P.g x - (P.ε⁻¹ * ↑(x ^ (-P.k))) • P.f₀

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

def WeakFEPair.toStrongFEPair {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (P : WeakFEPair E) : StrongFEPair E

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

def WeakFEPair.Λ₀ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (P : WeakFEPair E) : ℂ → E

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

• P.Λ₀ = mellin P.f_modif

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.differentiable_Λ₀ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (P : WeakFEPair E) : Differentiable ℂ P.Λ₀

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) : DifferentiableAt ℂ P.Λ s

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₀.