@[simp]

theorem Complex.norm_ofReal (x : ℝ) : ‖↑x‖ = |x|

@[simp]

theorem Complex.ennreal_norm_eq (z : ℂ) : ‖z‖ₑ = ↑‖z‖₊

@[simp]

theorem Complex.ennreal_norm_mul_self (z : ℂ) : ‖z‖ₑ * ‖z‖ₑ = ↑‖z‖₊ * ↑‖z‖₊

Core Mellin-Plancherel Theorems

This section contains the fundamental theorems of Mellin-Plancherel theory that establish Uσ as an isometry between Hσ and L²(ℝ).

noncomputable def Frourio.LogPull (σ : ℝ) (f : ↥(Hσ σ)) : ℝ → ℂ

Logarithmic pullback from Hσ to unweighted L²(ℝ). We transport along x = exp t and incorporate the Jacobian/weight factor so that ‖LogPull σ f‖_{L²(ℝ)} = ‖f‖_{Hσ}. Explicitly, (LogPull σ f)(t) = e^{(σ - 1/2) t} · f(e^t).

Equations

• Frourio.LogPull σ f t = ↑(Real.exp ((σ - 1 / 2) * t)) * Hσ.toFun f (Real.exp t)

@[simp]

theorem Frourio.LogPull_apply (σ : ℝ) (f : ↥(Hσ σ)) (t : ℝ) : LogPull σ f t = ↑(Real.exp ((σ - 1 / 2) * t)) * Hσ.toFun f (Real.exp t)

theorem Frourio.weight_measurable (σ : ℝ) : Measurable fun (t : ℝ) => ENNReal.ofReal (Real.exp (2 * σ * t))

Helper lemma: the weight function is measurable

theorem Frourio.LogPull_measurable (σ : ℝ) (f : ↥(Hσ σ)) : Measurable (LogPull σ f)

Helper lemma: LogPull preserves measurability

theorem Frourio.LogPull_norm_sq (σ : ℝ) (f : ↥(Hσ σ)) (t : ℝ) : ‖LogPull σ f t‖ ^ 2 = Real.exp ((2 * σ - 1) * t) * ‖Hσ.toFun f (Real.exp t)‖ ^ 2

theorem Frourio.LogPull_integrand_eq (σ : ℝ) (f : ↥(Hσ σ)) (t : ℝ) : ↑‖LogPull σ f t‖₊ ^ 2 = ENNReal.ofReal (‖Hσ.toFun f (Real.exp t)‖ ^ 2) * ENNReal.ofReal (Real.exp ((2 * σ - 1) * t))

theorem Frourio.LogPull_isometry (σ : ℝ) (f : ↥(Hσ σ)) : ‖f‖ ^ 2 = (∫⁻ (x : ℝ) in Set.Ioi 0, ↑‖Hσ.toFun f x‖₊ ^ 2 * ENNReal.ofReal (x ^ (2 * σ - 1) / x)).toReal

Isometry identity for Hσ: a concrete norm formula. This version exposes the Hσ-norm as an explicit weighted integral on (0,∞). It serves as the measurable backbone for the logarithmic substitution step in plan0.

theorem Frourio.Hσ_zero_integral (σ : ℝ) : ∫⁻ (x : ℝ) in Set.Ioi 0, ↑‖Hσ.toFun 0 x‖₊ ^ 2 * ENNReal.ofReal (x ^ (2 * σ - 1) / x) = 0

When f = 0 in Hσ, the L2 integral of its squared norm is 0

theorem Frourio.LogPull_memLp (σ : ℝ) (f : ↥(Hσ σ)) : MeasureTheory.MemLp (LogPull σ f) 2 MeasureTheory.volume

theorem Frourio.mellin_in_L2 (σ : ℝ) (f : ↥(Hσ σ)) : MeasureTheory.MemLp (LogPull σ f) 2 MeasureTheory.volume

The Mellin transform of an L² function on ℝ₊ with weight t^(2σ-1) belongs to L²(ℝ) when evaluated along the critical line Re(s) = σ

theorem Frourio.mellin_direct_isometry (σ : ℝ) : ∃ C > 0, ∀ (f : ↥(Hσ σ)), ∫ (τ : ℝ), ‖LogPull σ f τ‖ ^ 2 = C * ‖f‖ ^ 2

Direct isometry theorem: The Mellin transform preserves L² norm

theorem Frourio.mellin_plancherel_formula (σ : ℝ) (f : ↥(Hσ σ)) : ∃ C > 0, ∫ (τ : ℝ), ‖LogPull σ f τ‖ ^ 2 = C * ‖f‖ ^ 2

Mellin-Plancherel Formula: The Mellin transform preserves the L² norm up to a constant factor depending on σ

theorem Frourio.exp_weight_cancel (σ τ : ℝ) : ↑(Real.exp ((σ - 1 / 2) * τ)) * ↑(Real.exp τ) ^ (-(↑σ - ↑(1 / 2))) = 1

Auxiliary identity: the Jacobian weight appearing in LogPull cancels with the inverse weight built into toHσ_ofL2.