3.3. The radial Mellin transform
The radial Mellin transform, its logarithmic-profile description, and the Mellin–Hankel functional equation (Section 2.2 of the report).
Set \lambda = d/2 and S_d = 2\pi^{d/2}/\Gamma(d/2), the area of the unit sphere
(S_d = d\,v_d with v_d from Definition 1.1.3).
Lean code for Definition3.3.1●1 definition
Associated Lean declarations
-
CohnElkies.sphereArea[complete]
-
CohnElkies.sphereArea[complete]
-
defdefined in CohnElkies/Radial.leancomplete
def CohnElkies.sphereArea (d : ℕ) : ℝ
def CohnElkies.sphereArea (d : ℕ) : ℝ
The surface area `S_d = d v_d` of the unit sphere of `ℝ^d`.
For radial g with profile g(r), polar integration gives
\int_{\mathbb{R}^d} g(x)|x|^{s-d}\,dx = S_d\int_0^\infty g(r)\,r^{s-1}\,dr whenever either
side converges absolutely, with S_d from Definition 3.3.1; in particular
\int_{\mathbb{R}^d} g(x)\,dx = S_d\int_0^\infty g(r)\,r^{d-1}\,dr for integrable radial g.
Lean code for Lemma3.3.2●1 theorem
Associated Lean declarations
-
CohnElkies.integral_radialProfile_cpow[complete]
-
CohnElkies.integral_radialProfile_cpow[complete]
-
theoremdefined in CohnElkies/Radial.leancomplete
theorem CohnElkies.integral_radialProfile_cpow {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) (hf : CohnElkies.IsRadial ⇑f) (s : ℂ) : ∫ (x : CohnElkies.Euclidean d), f x * ↑‖x‖ ^ (s - ↑d) = CohnElkies.sphereArea d • mellin (CohnElkies.radialProfile hd f) s
theorem CohnElkies.integral_radialProfile_cpow {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) (hf : CohnElkies.IsRadial ⇑f) (s : ℂ) : ∫ (x : CohnElkies.Euclidean d), f x * ↑‖x‖ ^ (s - ↑d) = CohnElkies.sphereArea d • mellin (CohnElkies.radialProfile hd f) s
Polar integration for radial `f` with profile `g`: `∫ f(x) |x|^{s-d} dx = S_d · M g(s)` (report §2.2).
Integration in polar coordinates: the pushforward of Lebesgue measure under x \mapsto |x| has
density S_dr^{d-1} (Mathlib's MeasureTheory.integral_fun_norm_addHaar, with
\operatorname{vol}(B(0,1)) = v_d = S_d/d).
For \rho > 0 the Fourier transform of a radial function has the Hankel representation
\widehat g(\rho) = 2\pi\rho^{1-d/2}\int_0^\infty g(r)J_{d/2-1}(2\pi r\rho)\,r^{d/2}\,dr.
Because its Bessel kernel depends only on r\rho, the radial Fourier transform becomes
particularly simple after a Mellin transform: it reflects the Mellin variable and multiplies by an
explicit gamma factor. The functional equation below is proved here through Gaussian pairings and
Fubini rather than through the Hankel kernel, which is the route taken by the formalization.
For g \in \mathcal{S}_{\mathrm{rad}}(\mathbb{R}^d;\mathbb{R}) the radial profile is
r \mapsto g(re_1), and for \operatorname{Re} z > 0 its Mellin transform is (equation (8))
M_g(z) = \int_0^\infty g(r)\,r^{z-1}\,dr
(Mathlib's mellin of the profile; the integral converges absolutely since g is bounded
near 0 and rapidly decreasing).
Lean code for Definition3.3.3●1 definition
Associated Lean declarations
-
CohnElkies.radialProfile[complete]
-
CohnElkies.radialProfile[complete]
-
defdefined in CohnElkies/Radial.leancomplete
def CohnElkies.radialProfile {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) (r : ℝ) : ℂ
def CohnElkies.radialProfile {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) (r : ℝ) : ℂ
The radial profile `r ↦ f(r e₁)` of a test function `f` (the function `g(r)` of report §2.2).
The restriction of M_g (Definition 3.3.3) to the critical line is (equation (8))
X_g(t) = M_g(\lambda - it) for t \in \mathbb{R}.
Lean code for Definition3.3.4●1 definition
Associated Lean declarations
-
CohnElkies.X_fℝ[complete]
-
CohnElkies.X_fℝ[complete]
-
defdefined in CohnElkies/Radial.leancomplete
def CohnElkies.X_fℝ {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) (t : ℝ) : ℂ
def CohnElkies.X_fℝ {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) (t : ℝ) : ℂ
`X_f(t) = M g(λ - it)`: the Mellin transform of the radial profile `g` of `f` on the critical line `Re z = λ = d/2` (report (8)).
In the logarithmic radius v = \log r the critical log profile of g is
\Phi_g(v) = e^{\lambda v}g(e^v) (Definition 3.3.3). (The formalization uses the
reflected variable, u = -v: radialCriticalLogProfile is u \mapsto e^{-\lambda u}g(e^{-u}).)
Lean code for Definition3.3.5●1 definition
Associated Lean declarations
-
CohnElkies.radialCriticalLogProfile[complete]
-
CohnElkies.radialCriticalLogProfile[complete]
-
defdefined in CohnElkies/UpperBound/FourierPair.leancomplete
def CohnElkies.radialCriticalLogProfile {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) (u : ℝ) : ℂ
def CohnElkies.radialCriticalLogProfile {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) (u : ℝ) : ℂ
The critical log profile `u ↦ e^{-λu} g(e^{-u})`, `λ = d/2`, of the radial profile `g` of a test function `f`.
For g \in \mathcal{S}_{\mathrm{rad}}(\mathbb{R}^d;\mathbb{R}), the profile
r \mapsto g(re_1) is a Schwartz function on \mathbb{R} and
\Phi_g \in \mathcal{S}(\mathbb{R};\mathbb{R}) (Definition 3.3.5); in
particular \Phi_g and \widehat{\Phi_g} are integrable.
Lean code for Lemma3.3.6●3 declarations
Associated Lean declarations
-
defdefined in CohnElkies/Radial.leancomplete
def CohnElkies.radialSchwartzProfile {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) : SchwartzMap ℝ ℂ
def CohnElkies.radialSchwartzProfile {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) : SchwartzMap ℝ ℂ
The radial profile `r ↦ f(r e₁)` of a test function, as a Schwartz function on `ℝ`.
-
theoremdefined in CohnElkies/UpperBound/FourierPair.leancomplete
theorem CohnElkies.radialCriticalLogProfile_integrable {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) : MeasureTheory.Integrable (CohnElkies.radialCriticalLogProfile hd f) MeasureTheory.volume
theorem CohnElkies.radialCriticalLogProfile_integrable {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) : MeasureTheory.Integrable (CohnElkies.radialCriticalLogProfile hd f) MeasureTheory.volume
-
theoremdefined in CohnElkies/UpperBound/FourierPair.leancomplete
theorem CohnElkies.radialCriticalLogProfile_fourier_integrable {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) : MeasureTheory.Integrable (FourierTransform.fourier (CohnElkies.radialCriticalLogProfile hd f)) MeasureTheory.volume
theorem CohnElkies.radialCriticalLogProfile_fourier_integrable {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) : MeasureTheory.Integrable (FourierTransform.fourier (CohnElkies.radialCriticalLogProfile hd f)) MeasureTheory.volume
Smoothness of g at r = 0 gives exponential decay of \Phi_g and all its derivatives as
v \to -\infty, while the Schwartz decay of g gives rapid decay as v \to +\infty; thus
\Phi_g \in \mathcal{S}(\mathbb{R}). (The formalization proves only what is needed: the
profile is Schwartz as the composition of g with the isometry r \mapsto re_1, and
\Phi_g, an exponential tilt of a Schwartz function, and its Fourier transform are integrable.)
For g \in \mathcal{S}_{\mathrm{rad}}(\mathbb{R}^d;\mathbb{R}), with the notation of
Definition 3.3.4 and Definition 3.3.5,
X_g(t) = \int_{\mathbb{R}}\Phi_g(v)e^{-itv}\,dv: X_g is the Fourier transform of \Phi_g
(at the frequency t/(2\pi), with the convention of Definition 1.1.2).
Lean code for Lemma3.3.7●2 theorems
Associated Lean declarations
-
theoremdefined in CohnElkies/Radial.leancomplete
theorem CohnElkies.radialMellinFrequency_eq_fourier {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) (t : ℝ) : CohnElkies.X_fℝ hd f t = FourierTransform.fourier (fun u ↦ Real.exp (-(↑d / 2) * u) • CohnElkies.radialProfile hd f (Real.exp (-u))) (-t / (2 * Real.pi))
theorem CohnElkies.radialMellinFrequency_eq_fourier {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) (t : ℝ) : CohnElkies.X_fℝ hd f t = FourierTransform.fourier (fun u ↦ Real.exp (-(↑d / 2) * u) • CohnElkies.radialProfile hd f (Real.exp (-u))) (-t / (2 * Real.pi))
`X_f` is the Fourier transform of `v ↦ e^{-λ v} g(e^{-v})`. -
theoremdefined in CohnElkies/UpperBound/FourierPair.leancomplete
theorem CohnElkies.radialMellinFrequency_eq_criticalLogFourier {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) (t : ℝ) : CohnElkies.X_fℝ hd f t = FourierTransform.fourier (CohnElkies.radialCriticalLogProfile hd f) (-t / (2 * Real.pi))
theorem CohnElkies.radialMellinFrequency_eq_criticalLogFourier {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) (t : ℝ) : CohnElkies.X_fℝ hd f t = FourierTransform.fourier (CohnElkies.radialCriticalLogProfile hd f) (-t / (2 * Real.pi))
The substitution r = e^v in M_g(\lambda - it) = \int_0^\infty g(r)r^{\lambda-it-1}\,dr.
For g \in \mathcal{S}_{\mathrm{rad}}(\mathbb{R}^d;\mathbb{R}),
\Phi_g(v) = \dfrac{1}{2\pi}\int_{\mathbb{R}}X_g(t)e^{itv}\,dt, so that Mellin inversion reads
g(r) = \dfrac{r^{-\lambda}}{2\pi}\int_{\mathbb{R}} X_g(t)\,r^{it}\,dt
for r > 0 (Definition 3.3.4, Definition 3.3.5); in particular
g is determined by X_g.
Lean code for Lemma3.3.8●2 theorems
Associated Lean declarations
-
theoremdefined in CohnElkies/UpperBound/FourierPair.leancomplete
theorem CohnElkies.radialMellinFrequency_injective {d : ℕ} (hd : 0 < d) {f g : CohnElkies.TestFunction d} (hf : CohnElkies.IsRadial ⇑f) (hg : CohnElkies.IsRadial ⇑g) (hfrequency : ∀ (t : ℝ), CohnElkies.X_fℝ hd f t = CohnElkies.X_fℝ hd g t) : f = g
theorem CohnElkies.radialMellinFrequency_injective {d : ℕ} (hd : 0 < d) {f g : CohnElkies.TestFunction d} (hf : CohnElkies.IsRadial ⇑f) (hg : CohnElkies.IsRadial ⇑g) (hfrequency : ∀ (t : ℝ), CohnElkies.X_fℝ hd f t = CohnElkies.X_fℝ hd g t) : f = g
Report (8): a radial test function is determined by its Mellin frequency `X_f`.
-
theoremdefined in CohnElkies/UpperBound/FourierPair.leancomplete
theorem CohnElkies.criticalLogProfile_eq_fourierInv {d : ℕ} (hd : 0 < d) {F G : ℝ → ℂ} (hF : ∀ (r : ℝ), 0 < r → F r = ↑(r ^ (-(↑d / 2))) * FourierTransform.fourier G (Real.log r)) (f : CohnElkies.TestFunction d) (hf : ∀ (x : CohnElkies.Euclidean d), f x = F ‖x‖) : CohnElkies.radialCriticalLogProfile hd f = FourierTransformInv.fourierInv G
theorem CohnElkies.criticalLogProfile_eq_fourierInv {d : ℕ} (hd : 0 < d) {F G : ℝ → ℂ} (hF : ∀ (r : ℝ), 0 < r → F r = ↑(r ^ (-(↑d / 2))) * FourierTransform.fourier G (Real.log r)) (f : CohnElkies.TestFunction d) (hf : ∀ (x : CohnElkies.Euclidean d), f x = F ‖x‖) : CohnElkies.radialCriticalLogProfile hd f = FourierTransformInv.fourierInv G
If `f = F ‖·‖` with `F r = r^{-λ} 𝓕G(log r)` for `r > 0`, then the critical log profile of `f` is the inverse Fourier transform of `G`.
Ordinary one-dimensional Fourier inversion applied to Lemma 3.3.7
(\Phi_g and \widehat{\Phi_g} are integrable by Lemma 3.3.6);
rewriting it with r = e^v is the inversion formula (8). Injectivity follows since a radial
function is determined by its profile.
-
CohnElkies.fourier_zero_eq_integral[complete] -
CohnElkies.integral_radialProfile_cpow[complete]
For g \in \mathcal{S}_{\mathrm{rad}}(\mathbb{R}^d;\mathbb{R}),
\widehat g(0) = \int_{\mathbb{R}^d} g = S_d\,M_g(d) (Definition 3.3.3,
Lemma 3.3.2).
Lean code for Lemma3.3.9●2 theorems
Associated Lean declarations
-
CohnElkies.fourier_zero_eq_integral[complete]
-
CohnElkies.integral_radialProfile_cpow[complete]
-
CohnElkies.fourier_zero_eq_integral[complete] -
CohnElkies.integral_radialProfile_cpow[complete]
-
theoremdefined in CohnElkies/SignUncertainty/Mollifiers.leancomplete
theorem CohnElkies.fourier_zero_eq_integral {d : ℕ} (f : CohnElkies.Euclidean d → ℂ) : FourierTransform.fourier f 0 = ∫ (x : CohnElkies.Euclidean d), f x
theorem CohnElkies.fourier_zero_eq_integral {d : ℕ} (f : CohnElkies.Euclidean d → ℂ) : FourierTransform.fourier f 0 = ∫ (x : CohnElkies.Euclidean d), f x
-
theoremdefined in CohnElkies/Radial.leancomplete
theorem CohnElkies.integral_radialProfile_cpow {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) (hf : CohnElkies.IsRadial ⇑f) (s : ℂ) : ∫ (x : CohnElkies.Euclidean d), f x * ↑‖x‖ ^ (s - ↑d) = CohnElkies.sphereArea d • mellin (CohnElkies.radialProfile hd f) s
theorem CohnElkies.integral_radialProfile_cpow {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) (hf : CohnElkies.IsRadial ⇑f) (s : ℂ) : ∫ (x : CohnElkies.Euclidean d), f x * ↑‖x‖ ^ (s - ↑d) = CohnElkies.sphereArea d • mellin (CohnElkies.radialProfile hd f) s
Polar integration for radial `f` with profile `g`: `∫ f(x) |x|^{s-d} dx = S_d · M g(s)` (report §2.2).
The Fourier transform at 0 is the integral, and polar integration
(Lemma 3.3.2) with s = d.
(Mellin–Hankel functional equation.) For
g \in \mathcal{S}_{\mathrm{rad}}(\mathbb{R}^d;\mathbb{R})
and 0 < \operatorname{Re} z < d, with M as in Definition 3.3.3,
M_{\widehat g}(z) = \pi^{\lambda - z}\,\dfrac{\Gamma(z/2)}{\Gamma((d-z)/2)}\,M_g(d-z).
Lean code for Theorem3.3.10●1 theorem
Associated Lean declarations
-
CohnElkies.radial_fourier_mellin_strip[complete]
-
CohnElkies.radial_fourier_mellin_strip[complete]
-
theoremdefined in CohnElkies/MellinFourier.leancomplete
theorem CohnElkies.radial_fourier_mellin_strip {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) (hf : CohnElkies.IsRadial ⇑f) (s : ℂ) (hs : 0 < s.re) (hsd : s.re < ↑d) : mellin (CohnElkies.radialProfile hd (FourierTransform.fourier f)) s = ↑Real.pi ^ (↑d / 2 - s) * Complex.Gamma (s / 2) / Complex.Gamma ((↑d - s) / 2) * mellin (CohnElkies.radialProfile hd f) (↑d - s)
theorem CohnElkies.radial_fourier_mellin_strip {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) (hf : CohnElkies.IsRadial ⇑f) (s : ℂ) (hs : 0 < s.re) (hsd : s.re < ↑d) : mellin (CohnElkies.radialProfile hd (FourierTransform.fourier f)) s = ↑Real.pi ^ (↑d / 2 - s) * Complex.Gamma (s / 2) / Complex.Gamma ((↑d - s) / 2) * mellin (CohnElkies.radialProfile hd f) (↑d - s)
The Mellin–Hankel functional equation (9) of the report, for `0 < Re s < d`: `M ĝ(s) = π^{λ - s} Γ(s/2) / Γ((d-s)/2) · M g(d - s)` for the radial profile `g` of `f`.
For s > 0, the Gaussian \phi_s(y) = e^{-\pi|y|^2/s} has
\widehat{\phi_s}(x) = s^{\lambda}e^{-\pi s|x|^2} (Definition 1.1.2), and the
pairing identity \int g\,\widehat{\phi_s} = \int \widehat g\,\phi_s (Fubini;
CohnElkies.gaussianPairing_fourier) gives, after polar integration
(Lemma 3.3.2),
\int_0^\infty g(r)e^{-\pi s r^2}r^{d-1}\,dr
= s^{-\lambda}\int_0^\infty \widehat g(\rho)e^{-\pi\rho^2/s}\rho^{d-1}\,d\rho.
Multiply by s^{w-1} with 0 < \operatorname{Re} w < \lambda and integrate over
s \in (0,\infty); Tonelli applies since g, \widehat g are Schwartz and
d - 2\operatorname{Re} w > 0. On the left,
\int_0^\infty s^{w-1}e^{-\pi s r^2}\,ds = \Gamma(w)(\pi r^2)^{-w} gives
\Gamma(w)\pi^{-w}M_g(d-2w). On the right, the substitution s = 1/\sigma gives
\int_0^\infty s^{w-\lambda-1}e^{-\pi\rho^2/s}\,ds = \Gamma(\lambda-w)(\pi\rho^2)^{w-\lambda},
hence \Gamma(\lambda-w)\pi^{w-\lambda}M_{\widehat g}(2w) (CohnElkies.mellin_gaussianPairing,
CohnElkies.mellin_gaussianPairing_fourier). Setting z = 2w and solving for
M_{\widehat g}(z) yields the claim on 0 < \operatorname{Re} z < d; in the formalization the
intermediate identity is the Riesz pairing CohnElkies.fourier_riesz_pairing,
\Gamma((d-s)/2)\int \widehat f(\xi)|\xi|^{s-d}\,d\xi
= \pi^{\lambda-s}\Gamma(s/2)\int f(x)|x|^{-s}\,dx.
Let g \in \mathcal{S}_{\mathrm{rad}}(\mathbb{R}^d;\mathbb{R}) with g(0) = 0. Then
g(r) = O(r^2) as r \to 0, and M_g (Definition 3.3.3) converges and is
holomorphic on \operatorname{Re} z > -2.
Lean code for Lemma3.3.11●3 theorems
Associated Lean declarations
-
theoremdefined in CohnElkies/Radial.leancomplete
theorem CohnElkies.radialProfile_isBigO_rpow_two_zero {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) (hf : CohnElkies.IsRadial ⇑f) (hzero : f 0 = 0) : CohnElkies.radialProfile hd f =O[nhdsWithin 0 (Set.Ioi 0)] fun r ↦ r ^ 2
theorem CohnElkies.radialProfile_isBigO_rpow_two_zero {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) (hf : CohnElkies.IsRadial ⇑f) (hzero : f 0 = 0) : CohnElkies.radialProfile hd f =O[nhdsWithin 0 (Set.Ioi 0)] fun r ↦ r ^ 2
-
theoremdefined in CohnElkies/Radial.leancomplete
theorem CohnElkies.radialProfile_mellinConvergent {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) (hf : CohnElkies.IsRadial ⇑f) (hzero : f 0 = 0) (s : ℂ) (hs : -2 < s.re) : MellinConvergent (CohnElkies.radialProfile hd f) s
theorem CohnElkies.radialProfile_mellinConvergent {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) (hf : CohnElkies.IsRadial ⇑f) (hzero : f 0 = 0) (s : ℂ) (hs : -2 < s.re) : MellinConvergent (CohnElkies.radialProfile hd f) s
-
theoremdefined in CohnElkies/Radial.leancomplete
theorem CohnElkies.radialProfile_mellin_differentiableAt {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) (hf : CohnElkies.IsRadial ⇑f) (hzero : f 0 = 0) (s : ℂ) (hs : -2 < s.re) : DifferentiableAt ℂ (mellin (CohnElkies.radialProfile hd f)) s
theorem CohnElkies.radialProfile_mellin_differentiableAt {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) (hf : CohnElkies.IsRadial ⇑f) (hzero : f 0 = 0) (s : ℂ) (hs : -2 < s.re) : DifferentiableAt ℂ (mellin (CohnElkies.radialProfile hd f)) s
A smooth radial function is a smooth function of |x|^2, so g(r) = g(0) + O(r^2) = O(r^2);
the integral defining M_g(z) therefore converges absolutely and locally uniformly for
\operatorname{Re} z > -2, giving the holomorphic extension (Mathlib's
mellin_differentiableAt_of_isBigO_rpow).
Let g \in \mathcal{S}_{\mathrm{rad}}(\mathbb{R}^d;\mathbb{R}) with g(0) = 0. The
functional equation of Theorem 3.3.10, divided by the gamma factors, holds on the
closed strip 0 \le \operatorname{Re} z \le d:
\dfrac{M_{\widehat g}(z)}{\Gamma(z/2)} = \pi^{\lambda-z}\,\dfrac{M_g(d-z)}{\Gamma((d-z)/2)}
(Definition 3.3.3); on \operatorname{Re} z = 0 the apparent pole of
\Gamma(z/2) at z = 0 is thus harmless (if \widehat g(0) = 0, it is cancelled by the zero
M_g(d) = S_d^{-1}\widehat g(0) = 0).
Lean code for Lemma3.3.12●1 theorem
Associated Lean declarations
-
theoremdefined in CohnElkies/LowerBound/MellinStrip.leancomplete
theorem CohnElkies.radial_fourier_mellin_regularized_closed {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) (hf : CohnElkies.IsRadial ⇑f) (hzero : f 0 = 0) (hhatZero : (FourierTransform.fourier f) 0 = 0) (s : ℂ) (hs : 0 ≤ s.re) (hsd : s.re ≤ ↑d) : mellin (CohnElkies.radialProfile hd (FourierTransform.fourier f)) s * (Complex.Gamma (s / 2))⁻¹ = ↑Real.pi ^ (↑d / 2 - s) * (mellin (CohnElkies.radialProfile hd f) (↑d - s) * (Complex.Gamma ((↑d - s) / 2))⁻¹)
theorem CohnElkies.radial_fourier_mellin_regularized_closed {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) (hf : CohnElkies.IsRadial ⇑f) (hzero : f 0 = 0) (hhatZero : (FourierTransform.fourier f) 0 = 0) (s : ℂ) (hs : 0 ≤ s.re) (hsd : s.re ≤ ↑d) : mellin (CohnElkies.radialProfile hd (FourierTransform.fourier f)) s * (Complex.Gamma (s / 2))⁻¹ = ↑Real.pi ^ (↑d / 2 - s) * (mellin (CohnElkies.radialProfile hd f) (↑d - s) * (Complex.Gamma ((↑d - s) / 2))⁻¹)
The Mellin–Fourier functional equation (9) of the report in regularized form, extended from the open strip `0 < Re s < d` to its closure by continuity.
By Lemma 3.3.11, M_g is holomorphic on
\operatorname{Re} z > -2, and the same applies to \widehat g, which is radial Schwartz with
\widehat g(0) = 0. The right-hand side of (9) is holomorphic on
-2 < \operatorname{Re} z < d+2 except for the simple pole of \Gamma(z/2) at z = 0, which
is removable because M_g(d) = 0 (Lemma 3.3.9). Both sides agree on
0 < \operatorname{Re} z < d by Theorem 3.3.10, hence everywhere on the
connected strip by the identity theorem; the regularized form follows by continuity of both
sides on the closed strip.
The line \operatorname{Re} z = d/2 is fixed by the reflection z \mapsto d - z. For
g \in \mathcal{S}_{\mathrm{rad}}(\mathbb{R}^d;\mathbb{R}) and t \in \mathbb{R},
X_{\widehat g}(t) = m_\lambda(t)\,X_g(-t), where
m_\lambda(t) = \pi^{it}\,\dfrac{\Gamma((\lambda - it)/2)}{\Gamma((\lambda + it)/2)}
(equation (10)), a unimodular multiplier.
Lean code for Lemma3.3.13●1 theorem
Associated Lean declarations
-
CohnElkies.radialMellinMultiplier[complete]
-
CohnElkies.radialMellinMultiplier[complete]
-
theoremdefined in CohnElkies/MellinFourier.leancomplete
theorem CohnElkies.radialMellinMultiplier {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) (hf : CohnElkies.IsRadial ⇑f) (t : ℝ) : CohnElkies.X_fℝ hd (FourierTransform.fourier f) t = CohnElkies.m_ℓ (↑d / 2) t * CohnElkies.X_fℝ hd f (-t)
theorem CohnElkies.radialMellinMultiplier {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) (hf : CohnElkies.IsRadial ⇑f) (t : ℝ) : CohnElkies.X_fℝ hd (FourierTransform.fourier f) t = CohnElkies.m_ℓ (↑d / 2) t * CohnElkies.X_fℝ hd f (-t)
The Mellin multiplier identity (10) of the report: `X_{𝓕 f}(t) = m_λ(t) X_f(-t)`.
Evaluate Theorem 3.3.10 at z = \lambda - it, for which d - z = \lambda + it
and X_g(-t) = M_g(\lambda + it) (Definition 3.3.4). The properties of m_\lambda
follow from \Gamma(\bar z) = \overline{\Gamma(z)} (Lemma 3.1.1) and
|\pi^{it}| = 1.