Appendix E: Mellin–Sobolev algebra skeleton (H^s_×)

We provide lightweight signatures only, avoiding heavy analysis. The carrier is modeled as ℝ → ℂ, with a placeholder norm. Algebraicity and scale-action are recorded as Prop statements for later proof.

@[reducible, inline]

abbrev Frourio.Htimes (_s : ℝ) : Type

Equations

• Frourio.Htimes _s = (ℝ → ℂ)

noncomputable def Frourio.HtimesNorm (_s : ℝ) (_f : Htimes _s) : ℝ

Equations

• Frourio.HtimesNorm _s _f = 0

def Frourio.algebraProp_Htimes (s : ℝ) : Prop

Algebra property: existence of a product bound constant C(s) so that the pointwise product stays in H^s_× with the usual estimate.

Equations

• Frourio.algebraProp_Htimes s = ∃ (C : ℝ), 0 ≤ C ∧ ∀ (f g : Frourio.Htimes s), (Frourio.HtimesNorm s fun (x : ℝ) => f x * g x) ≤ C * Frourio.HtimesNorm s f * Frourio.HtimesNorm s g

def Frourio.scaleProp_Htimes (s : ℝ) : Prop

Scale action statement: for α > 0, the scaling f ↦ (x ↦ f (α x)) acts boundedly on H^s_× with some constant depending on (α,s).

Equations

• Frourio.scaleProp_Htimes s = ∀ (α : ℝ), 0 < α → ∃ (C : ℝ), 0 ≤ C ∧ ∀ (f : Frourio.Htimes s), (Frourio.HtimesNorm s fun (x : ℝ) => f (α * x)) ≤ C * Frourio.HtimesNorm s f