Generating Functional and Schwinger Functions

Defines the generating functional Z[J] = ∫ exp(i⟨ω,J⟩) dμ(ω) and Schwinger n-point functions Sₙ(f₁,...,fₙ) = ∫ ⟨ω,f₁⟩...⟨ω,fₙ⟩ dμ(ω).

For centered Gaussian measures: Z[J] = exp(−½⟨J,CJ⟩) and all Sₙ are determined by Wick's theorem from the two-point function S₂ = C.

Schwinger Functions

The Schwinger functions S_n are the n-th moments of field operators φ(f₁)...φ(fₙ) where φ(f) = ⟨ω, f⟩ is the field operator defined by pairing the field configuration with a test function.

Following Glimm and Jaffe, these are the fundamental correlation functions: S_n(f₁,...,fₙ) = ∫ ⟨ω,f₁⟩ ⟨ω,f₂⟩ ... ⟨ω,fₙ⟩ dμ(ω)

The Schwinger functions contain all the physics and satisfy the OS axioms. They can be obtained from the generating functional via exponential series: S_n(f₁,...,fₙ) = (-i)ⁿ (coefficient of (iJ)ⁿ/n! in Z[J])

noncomputable def SchwingerFunction (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) (n : ℕ) (f : Fin n → TestFunction) : ℝ

The n-th Schwinger function: n-point correlation function of field operators. S_n(f₁,...,fₙ) = ∫ ⟨ω,f₁⟩ ⟨ω,f₂⟩ ... ⟨ω,fₙ⟩ dμ(ω)

This is the fundamental object in constructive QFT - all physics is contained in the infinite sequence of Schwinger functions {S_n}_{n=1}^∞.

Equations

• SchwingerFunction dμ_config n f = ∫ (ω : FieldConfiguration), ∏ i : Fin n, distributionPairing ω (f i) ∂↑dμ_config

noncomputable def SchwingerFunction₁ (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) (f : TestFunction) : ℝ

The 1-point Schwinger function: the mean field

Equations

• SchwingerFunction₁ dμ_config f = SchwingerFunction dμ_config 1 ![f]

noncomputable def SchwingerFunction₂ (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) (f g : TestFunction) : ℝ

The 2-point Schwinger function: the covariance

Equations

• SchwingerFunction₂ dμ_config f g = SchwingerFunction dμ_config 2 ![f, g]

theorem schwinger_eq_mean (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) (f : TestFunction) : SchwingerFunction₁ dμ_config f = GJMean dμ_config f

The Schwinger function equals the GJ mean for n=1

theorem schwinger_eq_covariance (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) (f g : TestFunction) : SchwingerFunction₂ dμ_config f g = ∫ (ω : FieldConfiguration), distributionPairing ω f * distributionPairing ω g ∂↑dμ_config

The Schwinger function equals the direct covariance integral for n=2

theorem schwinger_vanishes_centered (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) (h_centered : ∀ (f : TestFunction), GJMean dμ_config f = 0) (f : TestFunction) : SchwingerFunction₁ dμ_config f = 0

For centered measures (zero mean), the 1-point function vanishes

noncomputable def SchwingerFunctionℂ (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) (n : ℕ) (f : Fin n → TestFunctionℂ) : ℂ

Complex version of Schwinger functions for complex test functions

Equations

• SchwingerFunctionℂ dμ_config n f = ∫ (ω : FieldConfiguration), ∏ i : Fin n, distributionPairingℂReal ω (f i) ∂↑dμ_config

noncomputable def SchwingerFunctionℂ₂ (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) (φ ψ : TestFunctionℂ) : ℂ

The complex 2-point Schwinger function for complex test functions. This is the natural extension of SchwingerFunction₂ to complex test functions.

Equations

• SchwingerFunctionℂ₂ dμ_config φ ψ = SchwingerFunctionℂ dμ_config 2 ![φ, ψ]

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

Property that SchwingerFunctionℂ₂ is ℂ-bilinear in both arguments. This is a key property for Gaussian measures and essential for OS0 analyticity.

Equations

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

theorem CovarianceBilinear_of_integrable (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) (h_int : ∀ (φ ψ : TestFunctionℂ), MeasureTheory.Integrable (fun (ω : FieldConfiguration) => distributionPairingℂReal ω φ * distributionPairingℂReal ω ψ) ↑dμ_config) : CovarianceBilinear dμ_config

If the product pairing is integrable for all test functions, then the complex 2-point Schwinger function is ℂ-bilinear in both arguments.

Exponential Series Connection to Generating Functional

The key insight: Instead of functional derivatives, we use the constructive exponential series: Z[J] = ∫ exp(i⟨ω, J⟩) dμ(ω) = ∑_{n=0}^∞ (i)^n/n! * S_n(J,...,J)

This approach is more elementary and constructive than functional derivatives.

def IsGaussianMeasure (dμ : MeasureTheory.ProbabilityMeasure FieldConfiguration) : Prop

A (centered) Gaussian field measure: the generating functional is an exponential of a quadratic form.

Equations

• IsGaussianMeasure dμ = ∃ (Cov : TestFunction → TestFunction → ℝ), ∀ (J : TestFunction), GJGeneratingFunctional dμ J = Complex.exp (-1 / 2 * ↑(Cov J J))

Basic Distribution Framework

The following definitions provide the foundation for viewing Schwinger functions as distributions on product spaces. These are needed by other modules.

@[reducible, inline]

abbrev SpaceTimeProduct (n : ℕ) : Type

The product space of n copies of spacetime

Equations

• SpaceTimeProduct n = (Fin n → SpaceTime)

@[reducible, inline]

abbrev TestFunctionProduct (n : ℕ) : Type

Test functions on the n-fold product space

Equations

• TestFunctionProduct n = SchwartzMap (SpaceTimeProduct n) ℝ