Multiplicative Convolution and Involution on ℝ₊*

Defines multiplicative convolution (g ⋆ h)(x) = ∫ g(y) h(x/y) d*y and involution g*(x) = conj(g(x⁻¹)) on positive reals. Proves involution is involutive and establishes Hölder-based integrability.

Reference: lamportform.tex, Section 1, lines 102–109.

def ConnesLean.mulConv (g h : RPos → ℂ) : RPos → ℂ

Multiplicative convolution of two functions on R_+*: (mulConv g h)(x) = integral g(y) * h(x/y) d*y.

We define this as a plain function RPos -> C, not as an Lp element, to allow pointwise evaluation (needed for Lemma 1).

Reference: lamportform.tex, lines 102-105.

Equations

• ConnesLean.mulConv g h x = ∫ (y : ConnesLean.RPos), g y * h (x / y) ∂ConnesLean.haarMult

def ConnesLean.mulInvol (g : RPos → ℂ) : RPos → ℂ

The involution g* : R_+* -> C defined by g*(x) = conj(g(x^{-1})).

Reference: lamportform.tex, lines 106-109.

Equations

• ConnesLean.mulInvol g x = (starRingEnd ℂ) (g x⁻¹)

theorem ConnesLean.mulInvol_involutive : Function.Involutive mulInvol

mulInvol is involutive: (g*)* = g.

@[simp]

theorem ConnesLean.mulInvol_mulInvol (g : RPos → ℂ) : mulInvol (mulInvol g) = g

Applying involution twice returns the original function.

theorem ConnesLean.mulConv_mulInvol_apply (g : RPos → ℂ) (a : RPos) : mulConv g (mulInvol g) a = ∫ (y : RPos), g y * (starRingEnd ℂ) (g (y / a)) ∂haarMult

Expand (mulConv g (mulInvol g))(a) to integral g(y) * conj(g(y/a)) d*y.

Reference: lamportform.tex, Lemma 1.1, Steps 1.1-1.3.

The key computation uses (a/y)^{-1} = y/a.

theorem ConnesLean.mulConv_mulInvol_integrable (g : RPos → ℂ) (hg : MeasureTheory.MemLp g 2 haarMult) (a : RPos) : MeasureTheory.Integrable (fun (y : RPos) => g y * (starRingEnd ℂ) (g (y / a))) haarMult

The integrand of mulConv g (mulInvol g) is integrable for g ∈ L²(d*x). Follows from Hölder's inequality applied to g and star(g ∘ (· / a)), both in L²(d*x), using measure-preservation of (· / a).