Mellin-Parseval Identity and its Relation to Fourier-Parseval

This file establishes the explicit relationship between the Mellin-Plancherel formula and the classical Fourier-Parseval identity through logarithmic change of variables.

Main Results

• mellin_to_fourier_change_of_variables: The change of variables x = e^t transforms the Mellin transform to a Fourier transform on the additive group ℝ
• parseval_identity_equivalence: The Mellin-Plancherel formula is equivalent to the Fourier-Parseval identity under appropriate transformation
• mellin_parseval_formula: Explicit Parseval formula for Mellin transforms

Implementation Notes

The key insight is that the multiplicative Haar measure dx/x on (0,∞) corresponds to the Lebesgue measure dt on ℝ under the logarithmic change of variables x = e^t.

noncomputable def Frourio.logMap : ↑(Set.Ioi 0) → ℝ

The logarithmic change of variables map

Equations

• Frourio.logMap x = Real.log ↑x

noncomputable def Frourio.expMap : ℝ → ↑(Set.Ioi 0)

The exponential change of variables map

Equations

• Frourio.expMap t = ⟨Real.exp t, ⋯⟩

noncomputable def Frourio.logMap_measurableEquiv : ↑(Set.Ioi 0) ≃ᵐ ℝ

The logarithmic map is a measurable equivalence

Equations

• One or more equations did not get rendered due to their size.

theorem Frourio.mellin_kernel_transform (s : ℂ) (t : ℝ) : ↑(Real.exp t) ^ (s - 1) = Complex.exp ((s - 1) * ↑t)

The Mellin kernel x^(s-1) becomes e^((s-1)t) under logarithmic change

theorem Frourio.mellin_change_of_variables (f : ℝ → ℂ) (s : ℂ) : ∫ (x : ℝ) in Set.Ioi 0, f x * ↑x ^ (s - 1) = ∫ (t : ℝ), f (Real.exp t) * ↑(Real.exp t) ^ (s - 1) * ↑(Real.exp t)

Change of variables lemma for Mellin transform: x = exp(t)

theorem Frourio.mellin_to_fourier_change_of_variables (f : ℝ → ℂ) (s : ℂ) : mellinTransform f s = ∫ (t : ℝ), f (Real.exp t) * Complex.exp (s * ↑t)

Under x = e^t, the Mellin transform becomes a Fourier-type transform

theorem Frourio.exp_image_measure_integral (E : Set ℝ) (hE : MeasurableSet E) : ∫⁻ (x : ℝ) in Real.exp '' E, ENNReal.ofReal (1 / x) = ∫⁻ (t : ℝ) in E, ENNReal.ofReal (1 / Real.exp t) * ENNReal.ofReal (Real.exp t)

Change of variables formula for exponential transformation

theorem Frourio.ennreal_div_exp_mul_exp (t : ℝ) : ENNReal.ofReal (1 / Real.exp t) * ENNReal.ofReal (Real.exp t) = 1

Simplification lemma: (1/exp(t)) * exp(t) = 1 in ENNReal

theorem Frourio.mulHaar_pushforward_log : ∃ (c : ENNReal), c ≠ 0 ∧ c ≠ ⊤ ∧ MeasureTheory.Measure.map Real.log (mulHaar.restrict (Set.Ioi 0)) = c • MeasureTheory.volume

The multiplicative Haar measure corresponds to Lebesgue measure

noncomputable def Frourio.logPushforward (f : ℝ → ℂ) : ℝ → ℂ

The transformed function under logarithmic change

Equations

• Frourio.logPushforward f t = f (Real.exp t)

noncomputable def Frourio.mellinWeight (σ : ℝ) : ℝ → ℝ

The weight function for the transformed inner product

Equations

• Frourio.mellinWeight σ t = Real.exp ((2 * σ - 1) * t)

theorem Frourio.mellin_as_weighted_fourier (f : ℝ → ℂ) (σ τ : ℝ) : mellinTransform f (↑σ + Complex.I * ↑τ) = ∫ (t : ℝ), logPushforward f t * Complex.exp (↑σ * ↑t) * Complex.exp (Complex.I * ↑τ * ↑t)

The Mellin transform at σ + iτ corresponds to weighted Fourier transform

theorem Frourio.complex_polarization_identity {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (f g : E) : 4 * inner ℂ f g = ↑(‖f + g‖ ^ 2) - ↑(‖f - g‖ ^ 2) - Complex.I * ↑(‖f + Complex.I • g‖ ^ 2) + Complex.I * ↑(‖f - Complex.I • g‖ ^ 2)

The polarization identity for complex inner products

theorem Frourio.mellin_logpull_relation (σ : ℝ) (f : ↥(Hσ σ)) (τ : ℝ) : mellinTransform (↑↑f) (↑σ + Complex.I * ↑τ) = ∫ (t : ℝ), LogPull σ f t * Complex.exp (Complex.I * ↑τ * ↑t) * Complex.exp (↑(1 / 2) * ↑t)

The Mellin transform relates to LogPull through change of variables

theorem Frourio.norm_simplification_logpull (σ : ℝ) (f : ↥(Hσ σ)) : ∫ (t : ℝ), ‖LogPull σ f t * Complex.exp (↑(1 / 2) * ↑t)‖ ^ 2 = ∫ (t : ℝ), ‖LogPull σ f t‖ ^ 2 * Real.exp t

Norm simplification for weighted LogPull

theorem Frourio.weighted_LogPull_integral_eq (σ : ℝ) (f : ↥(Hσ σ)) : ∫⁻ (t : ℝ), ENNReal.ofReal (‖LogPull σ f t * Complex.exp (↑(1 / 2) * ↑t)‖ ^ 2) = ∫⁻ (x : ℝ) in Set.Ioi 0, ENNReal.ofReal (‖↑↑f x‖ ^ 2 * x ^ (2 * σ - 1))

The L² norm of weighted LogPull equals the weighted L² norm of f, assuming the integral converges

def Frourio.has_weighted_L2_norm (σ : ℝ) (f : ↥(Hσ σ)) : Prop

Additional L² integrability condition for functions in Hσ σ

Equations

• Frourio.has_weighted_L2_norm σ f = (∫⁻ (x : ℝ) in Set.Ioi 0, ENNReal.ofReal (‖↑↑f x‖ ^ 2 * x ^ (2 * σ - 1)) < ⊤)

theorem Frourio.ennorm_sq_rpow (z : ℂ) : ‖z‖ₑ ^ 2 = ENNReal.ofReal (‖z‖ ^ 2)

Helper: relate ‖z‖ₑ squared (with real exponent) to ENNReal.ofReal (‖z‖^2).

theorem Frourio.weighted_LogPull_memLp (σ : ℝ) (f : ↥(Hσ σ)) (h_extra : has_weighted_L2_norm σ f) : MeasureTheory.MemLp (fun (t : ℝ) => LogPull σ f t * Complex.exp (↑(1 / 2) * ↑t)) 2 MeasureTheory.volume

The weighted LogPull function is in L² under suitable conditions

theorem Frourio.eLpNorm_triangle_diff (f g h : ℝ → ℂ) (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) (hg : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume) (hh : MeasureTheory.AEStronglyMeasurable h MeasureTheory.volume) : MeasureTheory.eLpNorm (f - h) 2 MeasureTheory.volume ≤ MeasureTheory.eLpNorm (f - g) 2 MeasureTheory.volume + MeasureTheory.eLpNorm (g - h) 2 MeasureTheory.volume

Triangle inequality for eLpNorm differences

theorem Frourio.mellin_transform_linear (σ : ℝ) (h k : ↥(Hσ σ)) (c s : ℂ) (hh_int : MeasureTheory.Integrable (fun (t : ℝ) => ↑↑h t * ↑t ^ (s - 1)) (MeasureTheory.volume.restrict (Set.Ioi 0))) (hk_int : MeasureTheory.Integrable (fun (t : ℝ) => ↑↑k t * ↑t ^ (s - 1)) (MeasureTheory.volume.restrict (Set.Ioi 0))) : mellinTransform (↑↑h + c • ↑↑k) s = mellinTransform (↑↑h) s + c * mellinTransform (↑↑k) s

Linearity of the Mellin transform (assuming convergence)