Translation Operator on L²(ℝ)

Defines the additive translation operator S_t φ(u) = φ(u - t) on L²(ℝ), the additive analogue of the dilation operator U_a via logarithmic coordinates. Proves measure preservation, L² norm invariance, and axiomatizes strong continuity of translations.

Reference: lamportform.tex, Section 2.

The translation operator

def ConnesLean.translationOp (t : ℝ) (φ : ℝ → ℂ) : ℝ → ℂ

The translation operator S_t on functions ℝ → ℂ, defined by (S_t φ)(u) = φ(u - t).

Reference: lamportform.tex, Section 2: additive translation on log coordinates.

Equations

• ConnesLean.translationOp t φ u = φ (u - t)

@[simp]

theorem ConnesLean.translationOp_apply (t : ℝ) (φ : ℝ → ℂ) (u : ℝ) : translationOp t φ u = φ (u - t)

@[simp]

theorem ConnesLean.translationOp_zero (φ : ℝ → ℂ) : translationOp 0 φ = φ

Translation by 0 is the identity.

theorem ConnesLean.translationOp_add (s t : ℝ) (φ : ℝ → ℂ) : translationOp s (translationOp t φ) = translationOp (s + t) φ

Translation is additive: S_s ∘ S_t = S_{s+t}.

theorem ConnesLean.dilation_eq_translation (t : ℝ) (g : RPos → ℂ) (u : ℝ) : dilationOp (expToRPos t) g (expToRPos u) = translationOp t (g ∘ expToRPos) u

Dilation on RPos conjugates to translation on ℝ via exp: (U_{exp(t)} g)(exp(u)) = (S_t (g ∘ exp))(u).

This is the key bridge between the multiplicative setup (Stage 1) and the additive setup (Stage 2).

L² properties of the translation operator

theorem ConnesLean.measurePreserving_sub_const (t : ℝ) : MeasureTheory.MeasurePreserving (fun (x : ℝ) => x - t) MeasureTheory.volume MeasureTheory.volume

Translation by t preserves Lebesgue measure on ℝ.

theorem ConnesLean.translationOp_lintegral_norm_eq (t : ℝ) (φ : ℝ → ℂ) : ∫⁻ (u : ℝ), ↑‖translationOp t φ u‖₊ ^ 2 = ∫⁻ (u : ℝ), ↑‖φ u‖₊ ^ 2

The L² norm is preserved under translation: ∫ ‖S_t φ‖² du = ∫ ‖φ‖² du.

Strong continuity of translations in L²

axiom ConnesLean.translation_norm_sq_continuous (φ : ℝ → ℂ) (hφ_meas : Measurable φ) (hφ_sq : ∫⁻ (u : ℝ), ↑‖φ u‖₊ ^ 2 < ⊤) : Continuous fun (t : ℝ) => ∫⁻ (u : ℝ), ↑‖φ u - translationOp t φ u‖₊ ^ 2

Axiom (Strong continuity of translations in L²): For measurable φ with finite L² norm, the map t ↦ ∫ ‖φ(u) − φ(u−t)‖² du is continuous.

This is a standard result: the translation group {S_t}_{t ∈ ℝ} is strongly continuous on L²(ℝ) (Engel-Nagel, Thm I.5.8).

Why axiom: Mathlib does not currently provide strong continuity of the translation group on Lp spaces. The proof requires density of continuous compactly supported functions in L² plus uniform continuity, or dominated convergence — both paths need unformalized infrastructure.

Soundness: All preconditions (measurability, finite L² norm) are standard analytic hypotheses matching Engel-Nagel Thm I.5.8. No structure parameters.

Reference: Engel-Nagel, One-Parameter Semigroups, Theorem I.5.8.