Log Coordinates: L² Isometry between ℝ₊* and ℝ

Establishes the L² isometry between (ℝ₊*, d*x) and (ℝ, du) via logarithmic coordinates. For g : ℝ₊* → ℂ supported on [λ⁻¹, λ], defines G = g ∘ exp supported on (-log λ, log λ) with ‖g‖²_{L²(d*x)} = ‖G‖²_{L²(du)}. Defines zeroExtend using Set.indicator.

Reference: lamportform.tex, Section 2.

Log interval and zero extension

def ConnesLean.logInterval (L : ℝ) : Set ℝ

The symmetric open interval (-L, L) in log coordinates. When L = log λ, this is the support of G = g ∘ exp for g supported on [λ⁻¹, λ].

Equations

• ConnesLean.logInterval L = Set.Ioo (-L) L

def ConnesLean.zeroExtend (G : ℝ → ℂ) (I : Set ℝ) : ℝ → ℂ

Zero-extend a function outside a set, using Set.indicator. zeroExtend G I u = G u if u ∈ I, and 0 otherwise.

Equations

• ConnesLean.zeroExtend G I = I.indicator G

@[simp]

theorem ConnesLean.zeroExtend_apply_mem {G : ℝ → ℂ} {I : Set ℝ} {u : ℝ} (hu : u ∈ I) : zeroExtend G I u = G u

@[simp]

theorem ConnesLean.zeroExtend_apply_nmem {G : ℝ → ℂ} {I : Set ℝ} {u : ℝ} (hu : u ∉ I) : zeroExtend G I u = 0

theorem ConnesLean.zeroExtend_eq_indicator (G : ℝ → ℂ) (I : Set ℝ) : zeroExtend G I = I.indicator G

theorem ConnesLean.measurableSet_logInterval (L : ℝ) : MeasurableSet (logInterval L)

The log interval is a measurable set.

L² isometry via exp equivalence

theorem ConnesLean.lintegral_norm_rpos_eq_real (g : RPos → ℂ) : ∫⁻ (x : RPos), ↑‖g x‖₊ ^ 2 ∂haarMult = ∫⁻ (u : ℝ), ↑‖g (expToRPos u)‖₊ ^ 2

The L² norm on (RPos, haarMult) equals the L² norm on (ℝ, volume) via the exponential change of variables: ∫ ‖g(x)‖² d*x = ∫ ‖g(exp u)‖² du.

theorem ConnesLean.lintegral_diff_dilation_eq_translation (g : RPos → ℂ) (a : RPos) : ∫⁻ (x : RPos), ↑‖g x - dilationOp a g x‖₊ ^ 2 ∂haarMult = ∫⁻ (u : ℝ), ↑‖(g ∘ expToRPos) u - translationOp (logFromRPos a) (g ∘ expToRPos) u‖₊ ^ 2

Translating the dilation norm difference to translation norm difference: ∫ ‖g(x) - g(x/a)‖² d*x = ∫ ‖G(u) - G(u - log a)‖² du where G = g ∘ exp.

This is the core identity connecting ‖g - U_a g‖² to ‖G - S_t G‖² in the additive picture.