Euclidean Group E(4) and Its Actions

Defines the Euclidean group E(4) = ℝ⁴ ⋊ O(4) with action g • x = R(x) + t on spacetime, and its induced actions on test functions (g • f)(x) = f(g⁻¹ • x).

Key properties: measure preservation (d⁴(E⁻¹x) = d⁴x), temperate growth of pullbacks (needed for Schwartz space), and continuity of all actions. Foundation for the OS2 axiom.

@[reducible, inline]

abbrev QFT.O4 : Type

Orthogonal linear isometries of ℝ⁴ (the group O(4)). LinearIsometry is an orthogonal linear map, ie an element of O(4)

Equations

• QFT.O4 = (SpaceTime →ₗᵢ[ℝ] SpaceTime)

Euclidean group

structure QFT.E : Type

Euclidean motion = rotation / reflection + translation. E= R^4 x O(4)

• R : O4

  Orthogonal linear part of the Euclidean motion.

• t : SpaceTime

  Translation part of the Euclidean motion.

noncomputable def QFT.act (g : E) (x : SpaceTime) : SpaceTime

Action of g : E on a spacetime point x. Impliments the pullback map x to Rx+ t

Equations

• QFT.act g x = g.R x + g.t

@[simp]

theorem QFT.act_one (x : SpaceTime) : act { R := 1, t := 0 } x = x

@[simp]

theorem QFT.act_mul (g h : E) (x : SpaceTime) : act { R := LinearIsometry.comp g.R h.R, t := g.R h.t + g.t } x = g.R (h.R x + h.t) + g.t

@[simp]

theorem QFT.act_inv (g : E) (x : SpaceTime) : act { R := g.R, t := -g.R g.t } x = g.R (x - g.t)

noncomputable def QFT.LinearIsometry.inv (g : O4) : O4

Inverse of a linear isometry : we turn the canonical equivalence (available in finite dimension) back into a LinearIsometry.

Equations

• QFT.LinearIsometry.inv g = (LinearIsometry.toLinearIsometryEquiv g QFT.LinearIsometry.inv._proof_4).symm.toLinearIsometry

@[simp]

theorem QFT.LinearIsometry.comp_apply (g h : O4) (x : SpaceTime) : (LinearIsometry.comp g h) x = g (h x)

@[simp]

theorem QFT.LinearIsometry.inv_apply (g : O4) (x : SpaceTime) : (inv g) (g x) = x

@[simp]

theorem QFT.LinearIsometry.one_apply (x : SpaceTime) : 1 x = x

@[simp]

theorem QFT.LinearIsometry.one_comp (R : O4) : LinearIsometry.comp 1 R = R

@[simp]

theorem QFT.LinearIsometry.comp_one (R : O4) : LinearIsometry.comp R 1 = R

@[simp]

theorem QFT.LinearIsometry.inv_comp (R : O4) : LinearIsometry.comp (inv R) R = 1

@[simp]

theorem QFT.LinearIsometry.comp_inv (R : O4) : LinearIsometry.comp R (inv R) = 1

theorem QFT.E.ext {g h : E} (hR : g.R = h.R) (ht : g.t = h.t) : g = h

theorem QFT.E.ext_iff {g h : E} : g = h ↔ g.R = h.R ∧ g.t = h.t

Group structure on E -----------------------------------------

@[implicit_reducible]

noncomputable instance QFT.instMulE : Mul E

Equations

• QFT.instMulE = { mul := fun (g h : QFT.E) => { R := LinearIsometry.comp g.R h.R, t := g.R h.t + g.t } }

@[implicit_reducible]

noncomputable instance QFT.instOneE : One E

Equations

• QFT.instOneE = { one := { R := 1, t := 0 } }

@[implicit_reducible]

noncomputable instance QFT.instInvE : Inv E

Equations

• QFT.instInvE = { inv := fun (g : QFT.E) => { R := QFT.LinearIsometry.inv g.R, t := -(QFT.LinearIsometry.inv g.R) g.t } }

@[implicit_reducible]

noncomputable instance QFT.instDivE : Div E

We need a Div instance because Group extends DivInvMonoid.

Equations

• QFT.instDivE = { div := fun (g h : QFT.E) => g * h⁻¹ }

@[simp]

theorem QFT.mul_R (g h : E) : (g * h).R = LinearIsometry.comp g.R h.R

@[simp]

theorem QFT.mul_t (g h : E) : (g * h).t = g.R h.t + g.t

@[simp]

theorem QFT.one_R : E.R 1 = 1

@[simp]

theorem QFT.one_t : E.t 1 = 0

@[simp]

theorem QFT.inv_R (g : E) : g⁻¹.R = LinearIsometry.inv g.R

@[simp]

theorem QFT.inv_t (g : E) : g⁻¹.t = -(LinearIsometry.inv g.R) g.t

@[implicit_reducible]

noncomputable instance QFT.instGroupE : Group E

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem QFT.act_mul_general (g h : E) (x : SpaceTime) : act (g * h) x = act g (act h x)

@[simp]

theorem QFT.act_inv_general (g : E) (x : SpaceTime) : act g⁻¹ (act g x) = x

Lebesgue measure is invariant under every Euclidean motion ---------

theorem QFT.measurePreserving_act (g : E) : MeasureTheory.MeasurePreserving (fun (x : SpaceTime) => act g x) μ μ

For every rigid motion g : E, the push‑forward of Lebesgue measure μ by the map x ↦ g • x is again μ. Equivalently, act g is measure‑preserving.

Unified Action of Euclidean group on function spaces ---------

UNIFIED EUCLIDEAN ACTION FRAMEWORK

This section demonstrates how the same geometric transformation (euclideanPullback)
can be used to define Euclidean actions on both test functions and L² functions:

1. **Common foundation**: All actions are based on the pullback map x ↦ g⁻¹ • x
2. **Key enabling result**: measurePreserving_act proves this map preserves Lebesgue measure
3. **Dual routes**:
   - Test functions: Use temperate growth + Schwartz space structure
   - L² functions: Use measure preservation + Lp space structure
4. **Unified interface**: Both yield continuous linear maps with the same group action laws

This approach eliminates code duplication and ensures consistency between
the test function and L² formulations of the Osterwalder-Schrader axioms.

noncomputable def QFT.euclideanPullback (g : E) : SpaceTime → SpaceTime

The fundamental pullback map for Euclidean actions. This is the geometric transformation x ↦ g⁻¹ • x that underlies all Euclidean actions on function spaces.

Equations

• QFT.euclideanPullback g = QFT.act g⁻¹

theorem QFT.euclidean_pullback_temperate_growth (g : E) : Function.HasTemperateGrowth (euclideanPullback g)

The Euclidean pullback map has temperate growth (needed for Schwartz space actions).

theorem QFT.euclidean_pullback_polynomial_bounds (g : E) : ∃ (k : ℕ) (C : ℝ), ∀ (x : SpaceTime), ‖x‖ ≤ C * (1 + ‖euclideanPullback g x‖) ^ k

The Euclidean pullback map satisfies polynomial growth bounds.

noncomputable def QFT.euclideanAction (g : E) (f : TestFunctionℂ) : TestFunctionℂ

Action of Euclidean group on test functions via pullback. For g ∈ E and f ∈ TestFunctionℂ, define (g • f)(x) = f(g⁻¹ • x). This is the standard pullback action: to evaluate the transformed function at x, we evaluate the original function at the inverse-transformed point.

Equations

• QFT.euclideanAction g f = (SchwartzMap.compCLM ℂ ⋯ ⋯) f

noncomputable def QFT.euclideanActionReal (g : E) (f : TestFunction) : TestFunction

Action of Euclidean group on real test functions via pullback. For g ∈ E and f ∈ TestFunction, define (g • f)(x) = f(g⁻¹ • x). This is the real version of euclideanAction for TestFunction = SchwartzMap SpaceTime ℝ.

Equations

• QFT.euclideanActionReal g f = (SchwartzMap.compCLM ℝ ⋯ ⋯) f

theorem QFT.euclidean_action_unified_basis (g : E) : MeasureTheory.MeasurePreserving (euclideanPullback g) μ μ

The measure preservation result enables both test function and L² actions. This is the key unifying lemma that works specifically for the spacetime measure μ.

noncomputable def QFT.euclideanActionL2 (g : E) (f : ↥(MeasureTheory.Lp ℂ 2 μ)) : ↥(MeasureTheory.Lp ℂ 2 μ)

Action of Euclidean group on L² functions via pullback. For g ∈ E and f ∈ Lp ℂ 2 μ, define (g • f)(x) = f(g⁻¹ • x). This uses the same fundamental pullback transformation as the test function action, but leverages measure preservation instead of temperate growth bounds. Specialized for SpaceTime with Lebesgue measure.

Equations

• QFT.euclideanActionL2 g f = (MeasureTheory.Lp.compMeasurePreserving (QFT.euclideanPullback g) ⋯) f

noncomputable def QFT.euclideanActionCLM (g : E) : TestFunctionℂ →L[ℂ] TestFunctionℂ

The Euclidean action as a continuous linear map on test functions. This leverages the Schwartz space structure and temperate growth bounds.

Equations

• QFT.euclideanActionCLM g = SchwartzMap.compCLM ℂ ⋯ ⋯

theorem QFT.euclidean_actions_unified (g : E) : (∃ (T_test : TestFunctionℂ →L[ℂ] TestFunctionℂ), ∀ (f : TestFunctionℂ), euclideanAction g f = T_test f) ∧ ∃ (T_L2 : ↥(MeasureTheory.Lp ℂ 2 μ) → ↥(MeasureTheory.Lp ℂ 2 μ)), ∀ (f : ↥(MeasureTheory.Lp ℂ 2 μ)), euclideanActionL2 g f = T_L2 f

Both actions are instances of the same abstract pattern.