Dilation Operator on L²(ℝ₊, dx)

Defines the dilation operator U_a g(x) = g(x/a) on L² with multiplicative Haar measure. Proves unitarity (isometry + surjectivity via U_a⁻¹ = U_{a⁻¹}), composition properties, and Cauchy-Schwarz bounds.

Reference: lamportform.tex, Section 1, lines 110–119.

def ConnesLean.dilationOp (a : RPos) (g : RPos → ℂ) : RPos → ℂ

The dilation operator U_a on functions RPos -> C, defined by (U_a g)(x) = g(x / a) for a in R_+*.

Reference: lamportform.tex, equation (1): (U_a g)(x) := g(x/a) for a > 0.

Equations

• ConnesLean.dilationOp a g x = g (x / a)

@[simp]

theorem ConnesLean.dilationOp_apply (a : RPos) (g : RPos → ℂ) (x : RPos) : dilationOp a g x = g (x / a)

@[simp]

theorem ConnesLean.dilationOp_one (g : RPos → ℂ) : dilationOp 1 g = g

Dilation at 1 is the identity.

theorem ConnesLean.dilationOp_mul (a b : RPos) (g : RPos → ℂ) : dilationOp a (dilationOp b g) = dilationOp (a * b) g

Dilation is multiplicative: U_a . U_b = U_{ab}.

theorem ConnesLean.dilationOp_inv (a : RPos) (g : RPos → ℂ) : dilationOp a⁻¹ (dilationOp a g) = g

U_{a^{-1}} is the inverse of U_a.

theorem ConnesLean.dilationOp_norm_eq (a : RPos) (g : RPos → ℂ) (_hg : MeasureTheory.MemLp g 2 haarMult) : ∫⁻ (x : RPos), ↑‖dilationOp a g x‖₊ ^ 2 ∂haarMult = ∫⁻ (x : RPos), ↑‖g x‖₊ ^ 2 ∂haarMult

The dilation operator is isometric on L^2(dx): ||U_a g||_2 = ||g||_2. This follows from Haar invariance: d(x/a) = d*x.

Reference: lamportform.tex, line 115-116.

theorem ConnesLean.inner_dilationOp_le (a : RPos) (g : RPos → ℂ) (hg : MeasureTheory.MemLp g 2 haarMult) : ‖∫ (x : RPos), g x * (starRingEnd ℂ) (dilationOp a g x) ∂haarMult‖ ≤ (∫⁻ (x : RPos), ↑‖g x‖₊ ^ 2 ∂haarMult).toReal

The Cauchy-Schwarz bound: |<g, U_a g>| <= ||g||_2^2.

Reference: lamportform.tex, line 118-119: |<g, U_a g>| <= ||g||_2 * ||U_a g||_2 = ||g||_2^2.