Gaussian Free Field Assembly

Defines muGFF m as a ProbabilityMeasure and proves two OS axioms for general Gaussian measures:

• OS0 (alternative via quadratic form): Z[∑ᵢ zᵢJᵢ] = exp(−½ ∑ᵢⱼ zᵢzⱼ⟨Jᵢ,CJⱼ⟩) is entire (the primary OS0 proof via Hartogs is in OS.os0Analyticity)
• OS2 (Euclidean invariance): Z[gf] = Z[f] when covariance is E(4)-invariant

OS0Alt Namespace

Alternative proof of OS0 for Gaussian measures via the explicit quadratic form expansion. The main proof used by OS.Master is in OS.os0Analyticity (holomorphic integral theorem).

theorem OS0Alt.bilin_sum_sum {E : Type u_2} [AddCommMonoid E] [Module ℂ E] (B : LinearMap.BilinMap ℂ E ℂ) (n : ℕ) (J : Fin n → E) (z : Fin n → ℂ) : (B (∑ i : Fin n, z i • J i)) (∑ j : Fin n, z j • J j) = ∑ i : Fin n, ∑ j : Fin n, z i * z j * (B (J i)) (J j)

Helper lemma for bilinear expansion with finite sums

def CovarianceContinuous (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) : Prop

Assumption: The complex covariance is continuous bilinear

Equations

• CovarianceContinuous dμ_config = ∀ (J K : TestFunctionℂ), Continuous fun (z : ℂ) => SchwingerFunctionℂ₂ dμ_config (z • J) K

OS0: Analyticity for Gaussian Measures (OLD PROOF - in OS0Alt namespace)

The key insight is that for Gaussian measures, the generating functional Z[∑ᵢ zᵢJᵢ] = exp(-½⟨∑ᵢ zᵢJᵢ, C(∑ⱼ zⱼJ⟩) = exp(-½ ∑ᵢⱼ zᵢzⱼ⟨Jᵢ, CJ⟩) is the exponential of a polynomial in the complex variables zᵢ, hence entire.

Note: The primary proof is in OSforGFF.OS.os0Analyticity.

noncomputable def OS0Alt.gjCovBilin (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) (h_bilinear : CovarianceBilinear dμ_config) : LinearMap.BilinMap ℂ TestFunctionℂ ℂ

The gjCovBilin declaration.

Equations

• OS0Alt.gjCovBilin dμ_config h_bilinear = LinearMap.mk₂ ℂ (fun (x y : TestFunctionℂ) => SchwingerFunctionℂ₂ dμ_config x y) ⋯ ⋯ ⋯ ⋯

theorem OS0Alt.gaussian_satisfies_OS0 (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) (h_gaussian : isGaussianGJ dμ_config) (h_bilinear : CovarianceBilinear dμ_config) : os0Analyticity dμ_config

OS2: Euclidean Invariance for Translation-Invariant Gaussian Measures

Euclidean invariance follows if the covariance operator commutes with Euclidean transformations. For translation-invariant measures, this is equivalent to the covariance depending only on differences of spacetime points.

def CovarianceEuclideanInvariant (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) : Prop

Assumption: The covariance is invariant under Euclidean transformations

Equations

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

def CovarianceEuclideanInvariantℂ (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) : Prop

Assumption: The complex covariance is invariant under Euclidean transformations

Equations

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

theorem gaussian_satisfies_OS2 (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) (h_gaussian : isGaussianGJ dμ_config) (h_euclidean_invariant : CovarianceEuclideanInvariantℂ dμ_config) : os2EuclideanInvariance dμ_config

Implementation Strategy

To complete these proofs, we need to:

1. Complete the Glimm-Jaffe reflection positivity argument:

   • Time reflection properly implemented using QFT.compTimeReflection from DiscreteSymmetry ✓
   • Implement covarianceOperator as the Riesz representation of the 2-point function
   • Complete the proof of glimm_jaffe_exponent_reflection_positive
   • Show that the 4-term expansion in the exponent has non-negative real part

2. Prove key lemmas:

   • Schwartz map composition with smooth transformations
   • Properties of the bilinear form distributionPairingℂReal
   • Continuity and analyticity of exponential functionals

3. Mathematical insights implemented:

   • OS0: Polynomial → exponential → entire function ✓
   • OS1: Positive semidefinite covariance → bounded generating functional ✓
   • OS2: Covariance commutes with transformations → generating functional invariant ✓
   • OS3: Reflection positivity framework following Glimm-Jaffe Theorem 6.2.2 ✓ (structure)
   • OS4: Covariance decay → correlation decay ✓

4. Glimm-Jaffe Theorem 6.2.2 Implementation:

   • Defined the key expansion: glimm_jaffe_exponent captures ⟨Fbar - CF', C(Fbar - CF')⟩
   • Structured the proof around the exponential form Z[Fbar - CF'] = exp(-½⟨Fbar - CF', C(Fbar - CF')⟩)
   • The reflection positivity condition ensures Re⟨Fbar - CF', C(Fbar - CF')⟩ ≥ 0
   • This gives |Z[Fbar - CF']| ≤ 1, which is the heart of reflection positivity

5. Connection to existing GFF work:

   • Use results from GFF.lean and GFF2.lean where applicable
   • Translate L2-based proofs to distribution framework
   • Leverage the explicit Gaussian form of the generating functional

Note: The main theorem gaussian_satisfies_all_GJ_OS_axioms shows that Gaussian measures satisfy all the OS axioms under appropriate assumptions on the covariance. The Glimm-Jaffe approach for OS3 provides the mathematical foundation for reflection positivity in the Gaussian Free Field context.