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.

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

• Strong FE pairs:

  • IsStrongFEPair.differentiable_Λ: Λ is entire
  • IsStrongFEPair.hasMellin: Λ is everywhere equal to the Mellin transform of f

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 : ℝ) : 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

structure IsStrongFEPair {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (P : WeakFEPair E) : Prop

A strong FE-pair is a weak FE-pair in which f₀ and g₀ are zero.

• hf₀ : P.f₀ = 0
• hg₀ : P.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.

noncomputable 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 := ⋯ }

@[simp]

theorem WeakFEPair.symm_g {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (P : WeakFEPair E) (a✝ : ℝ) : P.symm.g a✝ = P.f a✝

@[simp]

theorem WeakFEPair.symm_k {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (P : WeakFEPair E) : P.symm.k = P.k

@[simp]

theorem WeakFEPair.symm_f₀ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (P : WeakFEPair E) : P.symm.f₀ = P.g₀

@[simp]

theorem WeakFEPair.symm_f {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (P : WeakFEPair E) (a✝ : ℝ) : P.symm.f a✝ = P.g a✝

@[simp]

theorem WeakFEPair.symm_g₀ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (P : WeakFEPair E) : P.symm.g₀ = P.f₀

@[simp]

theorem WeakFEPair.symm_ε {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (P : WeakFEPair E) : P.symm.ε = P.ε⁻¹

@[simp]

theorem isStrongFEPair_symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {P : WeakFEPair E} : IsStrongFEPair P.symm ↔ IsStrongFEPair P

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

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 IsStrongFEPair.hf_top {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {P : WeakFEPair E} (hP : IsStrongFEPair P) (r : ℝ) : P.f =O[Filter.atTop] fun (x : ℝ) => x ^ r

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

theorem IsStrongFEPair.hf_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {P : WeakFEPair E} (hP : IsStrongFEPair P) (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.

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

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

noncomputable 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

theorem WeakFEPair.hf_modif_top {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (P : WeakFEPair E) (r : ℝ) : (fun (x : ℝ) => P.f_modif x - 0) =O[Filter.atTop] fun (x : ℝ) => x ^ r

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

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

(See WeakFEPair.isStrongFEPair_toStrongFEPair for the proof that this is actually a strong FE-pair.)

Equations

• P.toStrongFEPair = { f := P.f_modif, g := P.symm.f_modif, k := P.k, ε := P.ε, f₀ := 0, g₀ := 0, hf_int := ⋯, hg_int := ⋯, hk := ⋯, hε := ⋯, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ }

theorem WeakFEPair.isStrongFEPair_toStrongFEPair {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (P : WeakFEPair E) : IsStrongFEPair P.toStrongFEPair

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

noncomputable 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

noncomputable 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. (Compare IsStrongFEPair.hasMellin for a version without assumptions on s.re assuming the FE-pair is strong.)

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

Main theorems on strong FE-pairs

theorem IsStrongFEPair.Λ_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {P : WeakFEPair E} (hP : IsStrongFEPair P) : P.Λ = mellin P.f

For strong FE-pairs, P.Λ is everywhere equal to the Mellin transform of P.f.

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

theorem IsStrongFEPair.hasMellin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {P : WeakFEPair E} (hP : IsStrongFEPair P) (s : ℂ) : HasMellin P.f s (P.Λ s)

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

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

If P is a strong FE pair, then P.Λ is entire.