Mellin Transform Core Definitions

This file contains the core definitions for the Mellin transform theory that are needed by both MellinTransform and MellinBasic to avoid circular imports.

Main Definitions

• mulHaar: Haar measure on ℝ
• Hσ: Hilbert-Sobolev space
• zeroLatticeSpacing: Zero lattice spacing function

noncomputable def mulHaar : MeasureTheory.Measure ℝ

Multiplicative Haar measure on (0,∞)

Equations

• mulHaar = (MeasureTheory.volume.withDensity fun (x : ℝ) => ENNReal.ofReal (1 / x)).restrict (Set.Ioi 0)

@[reducible, inline]

noncomputable abbrev Hσ (σ : ℝ) : AddSubgroup (ℝ →ₘ[mulHaar.withDensity fun (x : ℝ) => ENNReal.ofReal (x ^ (2 * σ - 1))] ℂ)

Hilbert-Sobolev space Hσ

Equations

• Hσ σ = MeasureTheory.Lp ℂ 2 (mulHaar.withDensity fun (x : ℝ) => ENNReal.ofReal (x ^ (2 * σ - 1)))

noncomputable def Hσ.toFun {σ : ℝ} (f : ↥(Hσ σ)) : ℝ → ℂ

Coercion from Hσ to functions

Equations

• Hσ.toFun f = ↑↑f

noncomputable def zeroLatticeSpacing (Λ : ℝ) : ℝ

Zero lattice spacing

Equations

• zeroLatticeSpacing Λ = Real.pi / Real.log Λ