Lemma 1: Convolution Inner-Product Identity

Proves the four parts of Lemma 1 for f = g ⋆ g*:

1. f(a) = ⟨g, U_a g⟩ — convolution equals inner product with dilation
2. f(a⁻¹) = conj(f(a)) — conjugate symmetry
3. f(a) + f(a⁻¹) = 2 Re⟨g, U_a g⟩ — sum equals twice the real part
4. f(1) = ‖g‖² — norm at unity

Reference: lamportform.tex, Lemma 1.1 (lem:f-inner), lines 122–163.

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

Lemma 1, Part 1: f(a) = ⟨g, U_a g⟩_{L²(d*x)}.

The self-convolution (g ⋆ g*)(a) equals the inner product of g with its dilation U_a g.

Reference: lamportform.tex, Step 1 (lines 134–149).

Proof: Unfold convolution, apply involution definition, recognize as inner product with dilation operator.

theorem ConnesLean.convolution_inv_eq_conj (g : RPos → ℂ) (a : RPos) (_hg : MeasureTheory.MemLp g 2 haarMult) : mulConv g (mulInvol g) a⁻¹ = (starRingEnd ℂ) (mulConv g (mulInvol g) a)

Lemma 1, Part 2: f(a⁻¹) = conj(f(a)).

Reference: lamportform.tex, Step 2 (lines 150–156).

Proof: Replace a by a⁻¹, substitute y' = ya using Haar invariance.

theorem ConnesLean.convolution_add_inv (g : RPos → ℂ) (a : RPos) (hg : MeasureTheory.MemLp g 2 haarMult) : mulConv g (mulInvol g) a + mulConv g (mulInvol g) a⁻¹ = 2 * ↑(mulConv g (mulInvol g) a).re

Lemma 1, Part 3: f(a) + f(a⁻¹) = 2 Re⟨g, U_a g⟩.

Reference: lamportform.tex, Step 3, first part (lines 158–160).

Proof: Direct from Parts 1 and 2: z + conj(z) = 2 Re(z).

theorem ConnesLean.convolution_at_one (g : RPos → ℂ) (hg : MeasureTheory.MemLp g 2 haarMult) : mulConv g (mulInvol g) 1 = ↑(∫⁻ (x : RPos), ↑‖g x‖₊ ^ 2 ∂haarMult).toReal

Lemma 1, Part 4: f(1) = ‖g‖².

Reference: lamportform.tex, Step 3, second part (line 160).

Proof: At a = 1, U_1 = id, so ⟨g, U_1 g⟩ = ⟨g, g⟩ = ‖g‖².