Mellin transform phase (P2): definitions and lightweight scaffolding.

This file introduces the symbols and sets needed for the Mellin-analytic phase, without committing to heavy measure-theoretic proofs. Theorems that require integrability or operator-norm bounds are described in comments and will be proved in later phases once the analytic infrastructure is in place.

noncomputable def Frourio.mellinKernel (x : ℝ) (s : ℂ) : ℂ

Mellin kernel placeholder. Intended: (x : ℂ)^(s-1) on x>0. Kept minimal in P2 to avoid adding heavy dependencies.

Equations

• Frourio.mellinKernel x s = if 0 < x then ↑x ^ (s - 1) else 0

noncomputable def Frourio.mellinTransform (f : ℝ → ℂ) (s : ℂ) : ℂ

Mellin transform (signature).

Design intent: mellinTransform f s = ∫_{0}^{∞} f(x) x^{s-1} dx over ℝ. To keep this phase light and CI-friendly, we provide a placeholder value and fix the interface. The integral-based definition will be introduced in P3/P4.

Equations

• Frourio.mellinTransform f s = ∫ (t : ℝ) in Set.Ioi 0, f t * ↑t ^ (s - 1)

noncomputable def Frourio.phiSymbol (Λ : ℝ) (s : ℂ) : ℂ

Φ-difference Mellin symbol ϑ_Φ(Λ,s) := (Λ^{-s} - Λ^{s}) / (Λ - Λ^{-1}) (all coerced to ℂ).

Equations

• Frourio.phiSymbol Λ s = (Complex.exp (-s * ↑(Real.log Λ)) - Complex.exp (s * ↑(Real.log Λ))) / ↑(Λ - Λ⁻¹)

@[simp]

theorem Frourio.phiSymbol_at_zero (Λ : ℝ) : phiSymbol Λ 0 = 0

def Frourio.mellinZeros (Λ : ℝ) : Set ℂ

Zero lattice of the Φ-symbol on the imaginary axis (for Λ > 1). Formally: { s | ∃ k : ℤ, s = (iπ k) / log Λ } as complex numbers.

Equations

• Frourio.mellinZeros Λ = {s : ℂ | ∃ (k : ℤ), s = Complex.I * ↑Real.pi * ↑k / ↑(Real.log Λ)}

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

Golden lattice points on the real line: τₖ = k * (π / log φ).

Equations

• Frourio.goldenLatticePoint φ k = ↑k * zeroLatticeSpacing φ

def Frourio.isGoldenLattice (φ τ : ℝ) : Prop

Predicate that τ lies on the golden lattice generated by φ: ∃ k ∈ ℤ, τ = k * (π / log φ).

Equations

• Frourio.isGoldenLattice φ τ = ∃ (k : ℤ), τ = ↑k * zeroLatticeSpacing φ

@[simp]

theorem Frourio.isGoldenLattice_iff (φ τ : ℝ) : isGoldenLattice φ τ ↔ ∃ (k : ℤ), τ = ↑k * zeroLatticeSpacing φ

@[simp]

theorem Frourio.isGoldenLattice_zero (φ : ℝ) : isGoldenLattice φ 0

@[simp]

theorem Frourio.goldenLatticePoint_spec (φ : ℝ) (k : ℤ) : isGoldenLattice φ (goldenLatticePoint φ k)

theorem Frourio.log_ne_zero_of_one_lt {Λ : ℝ} (h : 1 < Λ) : Real.log Λ ≠ 0

If 1 < Λ then Real.log Λ ≠ 0.

theorem Frourio.denom_ne_zero_of_one_lt {Λ : ℝ} (h : 1 < Λ) : ↑(Λ - Λ⁻¹) ≠ 0

If 1 < Λ then the complex-coerced denominator is nonzero.

noncomputable def Frourio.Xiφ (φ : ℝ) (s : ℂ) : ℂ

Completed Xiφ (Weierstrass-normalized two-point symbol): Xiφ(φ,s) = (φ^{-s} − φ^{s}) / (−2 s log φ) as a function on ℂ. Note: At s=0 this has a removable singularity; we do not simplify it here.

Equations

• Frourio.Xiφ φ s = (Complex.exp (-s * ↑(Real.log φ)) - Complex.exp (s * ↑(Real.log φ))) / (-2 * s * ↑(Real.log φ))

theorem Frourio.div_eq_zero_of_ne {x c : ℂ} (hc : c ≠ 0) (hx : x / c = 0) : x = 0

Helper (Lemma A): for c ≠ 0 in ℂ, x / c = 0 implies x = 0.

theorem Frourio.div_eq_zero_iff_of_ne {x c : ℂ} (hc : c ≠ 0) : x / c = 0 ↔ x = 0

Helper (Lemma A, iff form): for c ≠ 0 in ℂ, x / c = 0 ↔ x = 0.

theorem Frourio.eq_div_iff_mul_eq_of_ne {a s r : ℂ} (ha : a ≠ 0) : s = r / a ↔ s * a = r

Helper (Lemma B): for a ≠ 0 in ℂ, s = r / a ↔ s * a = r.

theorem Frourio.exp_neg_eq_iff_exp_two_eq_one (w : ℂ) : Complex.exp (-w) = Complex.exp w ↔ Complex.exp (2 * w) = 1

Helper (Lemma C): exp (−w) = exp w iff exp (2w) = 1 over ℂ.

theorem Frourio.phiSymbol_zero_iff {Λ : ℝ} (hΛ : 1 < Λ) (s : ℂ) : phiSymbol Λ s = 0 ↔ s ∈ mellinZeros Λ

Algebraic zero-locus equivalence for phiSymbol under Λ > 1.

theorem Frourio.Xiφ_zero_iff {φ : ℝ} (hφ : 1 < φ) {s : ℂ} (hs : s ≠ 0) : Xiφ φ s = 0 ↔ s ∈ mellinZeros φ

Zero-locus equivalence for Xiφ away from the removable singularity at s=0. For 1 < φ and s ≠ 0, Xiφ φ s = 0 iff s lies on the imaginary lattice { i π k / log φ | k ∈ ℤ }.

def Frourio.VerticalLine (σ : ℝ) : Type

Vertical line Re s = σ as a subtype.

Equations

• Frourio.VerticalLine σ = { s : ℂ // s.re = σ }

noncomputable def Frourio.HσNorm (σ : ℝ) (u : ↥(Hσ σ)) : ℝ

The norm on H_σ induced from the L² structure with weighted measure. This is the standard L² norm with respect to the measure x^(2σ-1) dx/x on (0,∞).

Equations

• Frourio.HσNorm σ u = ‖u‖

noncomputable def Frourio.phiSymbolBound (Λ σ : ℝ) : ℝ

Candidate operator-norm bound expression (design quantity).

Equations

• Frourio.phiSymbolBound Λ σ = 2 * Real.cosh (σ * Real.log Λ) / (Λ - Λ⁻¹)

noncomputable def Frourio.divByX (g : ℝ → ℂ) : ℝ → ℂ

Helper: division by x for ℝ → ℂ functions.

Equations

• Frourio.divByX g x = g x / ↑x

noncomputable def Frourio.mellinPhiDiff (_Λ : ℝ) (f : ℝ → ℂ) : ℝ → ℂ

Φ-difference operator on the physical side (placeholder).

Equations

• Frourio.mellinPhiDiff _Λ f x = f x

noncomputable def Frourio.SmSymbol (m : ℕ) (Λ : ℝ) (s : ℂ) : ℂ

Concrete m-point Mellin-difference symbol phi_m as a finite linear combination of the two-point symbol phiSymbol with phase weights. The weights use m-th roots of unity exp(2π i j / m) and unit shifts in s. For m = 0, we set phi_m to 0 by convention.

Equations

• Frourio.SmSymbol m Λ s = if _h : m = 0 then 0 else ∑ j : Fin m, let w := Complex.exp (Complex.I * (2 * ↑Real.pi) * (↑↑↑j / ↑↑m)); w * Frourio.phiSymbol Λ (s + ↑↑j)

@[simp]

theorem Frourio.SmSymbol_zero_m (Λ : ℝ) (s : ℂ) : SmSymbol 0 Λ s = 0

def Frourio.SmZeros (_m : ℕ) (_Λ : ℝ) : Set ℂ

Design zero set for S_m (placeholder). In later phases this will be the corresponding arithmetic lattice generalizing mellinZeros for m=2.

Equations

• Frourio.SmZeros _m _Λ = {_s : ℂ | False}

def Frourio.Sm_zero_locus (m : ℕ) (Λ : ℝ) : Prop

Statement (as a Prop) that the zero-locus of S_m is described by SmZeros. No proof is provided at this phase.

Equations

• Frourio.Sm_zero_locus m Λ = ∀ (s : ℂ), Frourio.SmSymbol m Λ s = 0 ↔ s ∈ Frourio.SmZeros m Λ

def Frourio.IsBohrAlmostPeriodic (F : ℝ → ℂ) : Prop

Bohr almost periodicity predicate on ℝ → ℂ (minimalist version). We use a classical ε–T formulation of relatively dense ε-almost periods.

Equations

• Frourio.IsBohrAlmostPeriodic F = ∀ ε > 0, ∀ T > 0, ∃ (τ : ℝ), |τ| ≤ T ∧ ∀ (t : ℝ), ‖F (t + τ) - F t‖ < ε

def Frourio.Sm_bohr_almost_periodic (m : ℕ) (Λ σ : ℝ) : Prop

Statement (as a Prop) that the vertical-line trace of S_m is Bohr almost periodic. This captures the intended regularity in the design without committing to the full harmonic-analytic development at this stage.

Equations

• Frourio.Sm_bohr_almost_periodic m Λ σ = Frourio.IsBohrAlmostPeriodic fun (t : ℝ) => Frourio.SmSymbol m Λ (↑σ + Complex.I * ↑t)

Zero-locus equivalence for phiSymbol (Λ > 1) We provide a constructive proof via the periodicity of Complex.exp.