Frourio.Analysis.MellinPlancherelCore

Change of Variables Lemmas for Mellin-Plancherel #

These lemmas establish the key change of variables formulas needed for the logarithmic pullback map from L²(ℝ) to Hσ.

theorem Frourio.hx_id_helper (σ : ℝ) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (wσ : ℝ → ENNReal) (hwσ : wσ = fun (x : ℝ) => ENNReal.ofReal (x ^ (2 * σ - 1))) (g : ℝ → ℂ) (hg : g = fun (x : ℝ) => if x_1 : 0 < x then ↑↑f (Real.log x) * ↑x ^ (-(↑σ - ↑(1 / 2))) else 0) (x : ℝ) (hx : x ∈ Set.Ioi 0) :

↑‖g x‖₊ ^ 2 * wσ x * ENNReal.ofReal (1 / x) = ↑‖↑↑f (Real.log x)‖₊ ^ 2 * ENNReal.ofReal (1 / x)

source

theorem Frourio.enorm_to_nnnorm_lintegral (f : ℝ → ℂ) :

∫⁻ (t : ℝ), ‖f t‖ₑ ^ 2 = ∫⁻ (t : ℝ), ↑‖f t‖₊ ^ 2

ENorm to NNNorm conversion for complex functions

source

theorem Frourio.ofReal_norm_eq_coe_nnnorm (f : ℝ → ℂ) :

(fun (x : ℝ) => ENNReal.ofReal ‖f x‖ ^ 2) = fun (x : ℝ) => ↑‖f x‖₊ ^ 2

ENNReal.ofReal to coe conversion for norms

source

theorem Frourio.private_hg_memLp (σ : ℝ) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (wσ : ℝ → ENNReal) (hwσ : wσ = fun (x : ℝ) => ENNReal.ofReal (x ^ (2 * σ - 1))) (g : ℝ → ℂ) (hg : g = fun (x : ℝ) => if x_1 : 0 < x then ↑↑f (Real.log x) * ↑x ^ (-(↑σ - ↑(1 / 2))) else 0) :

MeasureTheory.MemLp g 2 (mulHaar.withDensity wσ)

Private lemma for extracting the MemLp proof needed in h_coe

source

theorem Frourio.private_h_coe (σ : ℝ) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) :

let wσ := fun (x : ℝ) => ENNReal.ofReal (x ^ (2 * σ - 1)); let g := fun (x : ℝ) => if x_1 : 0 < x then ↑↑f (Real.log x) * ↑x ^ (-(↑σ - ↑(1 / 2))) else 0; toHσ_ofL2 σ f = MeasureTheory.MemLp.toLp g ⋯

Private lemma for the h_coe equality in toHσ_ofL2_isometry

source

theorem Frourio.toHσ_ofL2_isometry (σ : ℝ) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) :

‖toHσ_ofL2 σ f‖ = ‖f‖

The embedding preserves the L² norm (isometry property). The logarithmic pullback is an isometry from L²(ℝ) to Hσ.

Step 3: 二点 Frourio 作用素の Mellin 側表現 #

We connect the Frourio operators from Algebra with the Mellin transform, establishing the multiplication operator representation.

source

theorem Frourio.phiSymbol_numerator_eq (φ : ℝ) (hφ : φ - φ⁻¹ ≠ 0) (s : ℂ) :

↑(φ - φ⁻¹) * phiSymbol φ s = Complex.exp (-s * ↑(Real.log φ)) - Complex.exp (s * ↑(Real.log φ))

Numerator identity for phiSymbol. Expands the defining fraction to an explicit numerator equality, avoiding commitment to a specific mellinSymbol normalization at this phase.

source

noncomputable def Frourio.Mφ (φ σ : ℝ) :

↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume) →L[ℂ ] ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

A simple bounded operator M_φ(σ) on L²(ℝ) given by scalar multiplication by the constant phiSymbol φ (σ : ℂ). This is a CI-friendly stand-in for the true τ-dependent multiplication operator f(τ) ↦ phiSymbol φ (σ + iτ) · f(τ). It is linear and bounded with operator norm ≤ ‖phiSymbol φ (σ : ℂ)‖.

Equations

Frourio.Mφ φ σ = Frourio.phiSymbol φ ↑σ • ContinuousLinearMap.id ℂ ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

Instances For

source

theorem Frourio.mellin_symbol_zero_lattice (φ : ℝ) (hφ : 1 < φ) (k : ℤ) :

phiSymbol φ (Complex.I * ↑Real.pi * ↑k / ↑(Real.log φ)) = 0

The Φ-symbol phiSymbol vanishes on the zero lattice (for φ > 1).

Step 4: 零格子と基本間隔の同定（完全証明） #

We strengthen and organize the zero lattice characterization, establishing the fundamental spacing π/log φ on the imaginary axis.

source

@[simp]

theorem Frourio.zeroLatticeSpacing_eq (φ : ℝ) :

zeroLatticeSpacing φ = Real.pi / Real.log φ

The fundamental spacing on the imaginary axis for the zero lattice

source

@[simp]

theorem Frourio.mem_mellinZeros_iff (φ : ℝ) (s : ℂ) :

s ∈ mellinZeros φ ↔ ∃ (k : ℤ), s = Complex.I * ↑Real.pi * ↑k / ↑(Real.log φ)

The zero lattice points are exactly iπk/log φ for integer k

source

theorem Frourio.phiSymbol_eq_zero_iff (φ : ℝ) (hφ : 1 < φ) (s : ℂ) :

phiSymbol φ s = 0 ↔ ∃ (k : ℤ), s = Complex.I * ↑Real.pi * ↑k / ↑(Real.log φ)

phiSymbol vanishes exactly on the zero lattice (strengthened version)

source

noncomputable def Frourio.latticePoint (φ : ℝ) (k : ℤ) :

ℂ

The k-th zero on the imaginary axis

Equations

Frourio.latticePoint φ k = Complex.I * ↑Real.pi * ↑k / ↑(Real.log φ)

Instances For

source

@[simp]

theorem Frourio.phiSymbol_latticePoint (φ : ℝ) (hφ : 1 < φ) (k : ℤ) :

phiSymbol φ (latticePoint φ k) = 0

latticePoint gives zeros of phiSymbol

source

theorem Frourio.latticePoint_spacing (φ : ℝ) (hφ : 1 < φ) (k : ℤ) :

latticePoint φ (k + 1) - latticePoint φ k = Complex.I * ↑(zeroLatticeSpacing φ)

The spacing between consecutive zeros

source

theorem Frourio.latticePoint_re (φ : ℝ) (k : ℤ) :

(latticePoint φ k).re = 0

The zeros are purely imaginary when restricted to the imaginary axis

source

theorem Frourio.latticePoint_im (φ : ℝ) (hφ : 1 < φ) (k : ℤ) :

(latticePoint φ k).im = Real.pi * ↑k / Real.log φ

The imaginary part of the k-th zero

source

@[simp]

theorem Frourio.latticePoint_neg (φ : ℝ) (k : ℤ) :

latticePoint φ (-k) = -latticePoint φ k

The zero lattice is symmetric about the origin

source

noncomputable def Frourio.goldenZeroLattice {φ : ℝ} :

Set ℂ

Export: The zero lattice for the golden ratio

Equations

Frourio.goldenZeroLattice = Frourio.mellinZeros φ

Instances For

source

noncomputable def Frourio.goldenSpacing {φ : ℝ} :

ℝ

The golden fundamental spacing

Equations

Frourio.goldenSpacing = zeroLatticeSpacing φ

Instances For

Step 5: Base Change Unitarity (底変更のユニタリ性) #

This section implements scale isometries for changing between different bases in the Mellin transform. The key insight is that rescaling τ ↦ c·τ in frequency space corresponds to a unitary transformation that allows conversion between different φ values.

Phase-2 Step 1: Base change and golden calibration.

We introduce the base-change linear isometric equivalence on L²(ℝ). For now, we keep the underlying action as the identity to stabilize API; the true scaling (baseChange c) g (t) = √c · g (c·t) will replace it in P3.

source