OS2 — Euclidean Invariance

Proves Z[Ef] = Z[f] for any Euclidean transformation E ∈ E(4). The argument:

1. Change variables x → E⁻¹x, y → E⁻¹y in the covariance integral
2. C(x,y) depends only on |x−y|, so C(E⁻¹x, E⁻¹y) = C(x,y)
3. Lebesgue measure is invariant: d⁴(E⁻¹x) = d⁴x (since |det R| = 1)

Hence S(Ef) = ∫∫ f*(x) C(x,y) f(y) dx dy = S(f).

Main results

• freeCovarianceℂ_bilinear_euclidean_invariant
• CovarianceEuclideanInvariantℂ_μ_GFF

Euclidean action on test functions

theorem QFT.euclidean_action_apply (g : E) (f : TestFunctionℂ) (x : SpaceTime) : (euclideanAction g f) x = f (euclideanPullback g x)

The Euclidean action satisfies (g • f)(x) = f(g⁻¹ • x).

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

The Euclidean pullback satisfies euclideanPullback g x = g⁻¹ • x = act g⁻¹ x.

theorem QFT.euclidean_pullback_act (g : E) (y : SpaceTime) : euclideanPullback g (act g y) = y

Composing pullbacks: euclideanPullback g (act g y) = y.

theorem QFT.act_euclidean_pullback (g : E) (x : SpaceTime) : act g (euclideanPullback g x) = x

The forward composition: act g (euclideanPullback g x) = x.

Change of variables for the bilinear form

noncomputable def QFT.actEquiv (g : E) : SpaceTime ≃ᵐ SpaceTime

The Euclidean action as a measurable equivalence.

Equations

• QFT.actEquiv g = { toFun := QFT.act g, invFun := QFT.act g⁻¹, left_inv := ⋯, right_inv := ⋯, measurable_toFun := ⋯, measurable_invFun := ⋯ }

theorem QFT.measurePreserving_actEquiv (g : E) : MeasureTheory.MeasurePreserving (⇑(actEquiv g)) MeasureTheory.volume MeasureTheory.volume

Measure-preserving property of actEquiv.

Main theorem: Bilinear form invariance

theorem QFT.freeCovarianceℂ_bilinear_euclidean_invariant (m : ℝ) (g : E) (f h : TestFunctionℂ) : freeCovarianceℂBilinear m (euclideanAction g f) (euclideanAction g h) = freeCovarianceℂBilinear m f h

The complex bilinear covariance form is invariant under Euclidean transformations. This is the key lemma showing ⟨g•f, C(g•h)⟩ = ⟨f, Ch⟩.

What needs to be proven: Starting from:

• freeCovariance_euclidean_invariant: C(g•x, g•y) = C(x, y) (proven in Covariance.lean)
• measurePreserving_act: act g preserves Lebesgue measure (proven in Euclidean.lean)

We need to show: ∫∫ f(g⁻¹•x) C(x,y) h(g⁻¹•y) dx dy = ∫∫ f(u) C(u,v) h(v) du dv

Proof sketch:

1. Rewrite C(x,y) = C(g•(g⁻¹•x), g•(g⁻¹•y)) using act_euclidean_pullback
2. Apply freeCovariance_euclidean_invariant to get C(g⁻¹•x, g⁻¹•y)
3. Now the integrand is F(g⁻¹•x, g⁻¹•y) where F(u,v) = f(u) C(u,v) h(v)
4. Change variables u = g⁻¹•x, v = g⁻¹•y (measure-preserving on product space)
5. Use MeasurePreserving.prod to get measure preservation on SpaceTime × SpaceTime

Technical gap: The Mathlib lemma MeasurePreserving.integral_comp' requires the integrand to have the form G(e x) for a MeasurableEquiv e. Our integrand after step 2 has the form f(g⁻¹•x) * C(g⁻¹•x, g⁻¹•y) * h(g⁻¹•y) which matches this pattern for the product integral ∫ F(e p.1, e p.2) d(p) where e = actEquiv g⁻¹.

Need to carefully apply integral_prod and MeasurePreserving.prod to complete.

theorem QFT.CovarianceEuclideanInvariantℂ_μ_GFF (m : ℝ) [Fact (0 < m)] : CovarianceEuclideanInvariantℂ (muGFF m)

The free GFF measure satisfies the complex covariance Euclidean invariance property. This removes the h_euc hypothesis from the master theorem.