OS0 — Analyticity of the Generating Functional

Proves that Z[∑ᵢ zᵢ fᵢ] = ∫ exp(i ∑ᵢ zᵢ ⟨φ, fᵢ⟩) dμ(φ) is analytic in the complex parameters zᵢ.

Strategy

For a centered Gaussian measure with covariance C, the complex generating functional has the closed form: Z[f] = exp(-½ C_ℂ(f, f)) where C_ℂ is the complexified covariance bilinear form (freeCovarianceℂBilinear).

Since C_ℂ is ℂ-bilinear: Z[∑ᵢ zᵢ Jᵢ] = exp(-½ ∑ᵢⱼ zᵢ zⱼ C_ℂ(Jᵢ, Jⱼ)) This is exp(quadratic polynomial in z), which is analytic on ℂⁿ.

Proof strategy for gff_complex_CF_covariance

1-parameter analytic continuation: decompose f = f_re + I·f_im, define L(t) = Z[f_re + t·f_im] and R(t) = exp(-½ Q(t)), show L = R on ℝ (from gff_real_characteristic), extend to ℂ via the identity theorem, evaluate at t = I.

Key Lemma

• gff_cf_slice_entire: t ↦ Z[f_re + t·f_im] is entire. Proved via Fernique integrability + parameter-dependent holomorphy of integrals.

Main result

• gaussianFreeField_satisfies_OS0

OS0 for the Gaussian Free Field

Preconditions for GFF Generating Functional Analyticity

These lemmas establish the preconditions needed for the analyticity proof. The generating functional is:

Z[J] = ∫ exp(i⟨ω, J⟩) dμ(ω)

where dμ is the Gaussian measure on field configurations.

theorem QFT.distributionPairingℂ_real_continuous (f : TestFunctionℂ) : Continuous fun (ω : FieldConfiguration) => distributionPairingℂReal ω f

The complex pairing is continuous in ω. This follows from the continuity of the evaluation map on WeakDual.

theorem QFT.distributionPairingℂ_real_measurable (f : TestFunctionℂ) : Measurable fun (ω : FieldConfiguration) => distributionPairingℂReal ω f

The complex pairing is measurable in ω (cylinder σ-algebra version). This follows from the measurability of the evaluation map on WeakDual.

theorem QFT.gff_integrand_measurable (m : ℝ) [Fact (0 < m)] (n : ℕ) (J : Fin n → TestFunctionℂ) (z : Fin n → ℂ) : MeasureTheory.AEStronglyMeasurable (fun (ω : FieldConfiguration) => Complex.exp (Complex.I * distributionPairingℂReal ω (∑ i : Fin n, z i • J i))) ↑(muGFF m)

The GFF integrand for the generating functional is measurable in ω for each z.

theorem QFT.gff_integrand_analytic (n : ℕ) (J : Fin n → TestFunctionℂ) (ω : FieldConfiguration) (z₀ : Fin n → ℂ) : AnalyticAt ℂ (fun (z : Fin n → ℂ) => Complex.exp (Complex.I * distributionPairingℂReal ω (∑ i : Fin n, z i • J i))) z₀

The GFF integrand is analytic in z for each fixed field configuration ω. This follows from the fact that:

1. z ↦ ∑ᵢ zᵢ • Jᵢ is linear (hence analytic) in z
2. ω ↦ ⟨ω, f⟩ is linear in f
3. exp(i · _) is entire

theorem QFT.norm_exp_I_distributionPairingℂ_real (f : TestFunctionℂ) (ω : FieldConfiguration) : ‖Complex.exp (Complex.I * distributionPairingℂReal ω f)‖ = Real.exp (-ω (complexTestFunctionDecompose f).2)

The norm of exp(I * distributionPairingℂReal ω f) equals exp(-(ω f_im)) where f_im is the imaginary part of the complex test function.

Proof: For a complex test function f with real/imaginary parts f_re, f_im:

• distributionPairingℂReal ω f = (ω f_re) + I * (ω f_im)
• I * distributionPairingℂReal ω f = I * (ω f_re) - (ω f_im)
• Re(I * distributionPairingℂReal ω f) = -(ω f_im)
• ‖exp(z)‖ = exp(Re(z)), so ‖exp(I * ...)‖ = exp(-(ω f_im))

theorem QFT.gff_exp_neg_pairing_integrable (m : ℝ) [Fact (0 < m)] (f : TestFunction) : MeasureTheory.Integrable (fun (ω : FieldConfiguration) => Real.exp (-ω f)) ↑(muGFF m)

Integrability of exp(-ω f) for a real test function f under the GFF measure. This follows from the Gaussian nature: for centered Gaussian X with variance σ², E[exp(-X)] = exp(σ²/2).

theorem QFT.gff_exp_abs_pairing_memLp (m : ℝ) [Fact (0 < m)] (f : TestFunction) (p : ENNReal) (hp : p ≠ ⊤) : MeasureTheory.MemLp (fun (ω : FieldConfiguration) => Real.exp |ω f|) p ↑(muGFF m)

exp(|ω f|) is in L^2 (and in fact all L^p) under the GFF measure. This follows from Fernique's theorem: if exp(α x²) is integrable, then exp(|x|)^p is integrable for all p < ∞ because |x|^p ≤ C_p * exp(ε x²) for small ε.

theorem QFT.gff_exp_abs_pairing_integrable (m : ℝ) [Fact (0 < m)] (f : TestFunction) : MeasureTheory.Integrable (fun (ω : FieldConfiguration) => Real.exp |ω f|) ↑(muGFF m)

Integrability of exp(|ω f|) under the GFF measure. This is the L¹ special case of gff_exp_abs_pairing_memLp.

theorem QFT.gff_exp_abs_sum_memLp (m : ℝ) [Fact (0 < m)] {ι : Type u_1} (s : Finset ι) (g : ι → TestFunction) : MeasureTheory.MemLp (fun (ω : FieldConfiguration) => Real.exp (∑ i ∈ s, |ω (g i)|)) 2 ↑(muGFF m)

Product of exponentials of absolute pairings is in L². If we have k test functions g₁, ..., gₖ, then exp(∑ᵢ |ω gᵢ|) = ∏ᵢ exp(|ω gᵢ|). Each exp(|ω gᵢ|) ∈ L^(2k) by gff_exp_abs_pairing_memLp. By generalized Hölder (MemLp.prod'), a product of k functions in L^(2k) is in L².

theorem QFT.gff_integrand_norm_integrable (m : ℝ) [Fact (0 < m)] (f : TestFunctionℂ) : MeasureTheory.Integrable (fun (ω : FieldConfiguration) => ‖Complex.exp (Complex.I * distributionPairingℂReal ω f)‖) ↑(muGFF m)

The integral of ‖exp(I * distributionPairingℂReal ω f)‖ is finite for any complex test function. This follows from the Gaussian exponential integrability applied to the imaginary part.

theorem QFT.gff_integrand_integrable (m : ℝ) [Fact (0 < m)] (n : ℕ) (J : Fin n → TestFunctionℂ) (z : Fin n → ℂ) : MeasureTheory.Integrable (fun (ω : FieldConfiguration) => Complex.exp (Complex.I * distributionPairingℂReal ω (∑ i : Fin n, z i • J i))) ↑(muGFF m)

The GFF integrand is integrable for each z. This follows from the norm being exp(-(ω f_im)) which is integrable by Gaussian exponential integrability.

Complex Characteristic Functional

The complex generating functional of the GFF equals exp(-½ C_ℂ(f,f)) where C_ℂ(f,g) = ∫∫ f(x) C(x,y) g(y) is the complexified covariance bilinear form.

This follows from the bivariate Gaussian MGF: for (X,Y) = (ω(f_re), ω(f_im)) jointly Gaussian, E[exp(iX - Y)] = exp(½(-Var(X) - 2i Cov(X,Y) + Var(Y))) which equals exp(-½ C_ℂ(f,f)).

theorem QFT.gff_cf_slice_entire (m : ℝ) [Fact (0 < m)] (f_re f_im : TestFunction) : AnalyticOnNhd ℂ (fun (t : ℂ) => GJGeneratingFunctionalℂ (muGFF m) (toComplex f_re + t • toComplex f_im)) Set.univ

The complex generating functional is analytic in a 1-parameter family. For fixed real f_re, f_im, the map t ↦ Z[toComplex f_re + t • toComplex f_im] is entire (analytic on all of ℂ).

This follows from: for each ω, the integrand exp(i⟨ω,f_re⟩ + it⟨ω,f_im⟩) is entire in t; the modulus is bounded by exp(|Im(t)| · |⟨ω,f_im⟩|), which is integrable by Fernique's theorem (gaussianFreeField_pairing_memLp). Standard parameter-dependent holomorphy then gives analyticity of the integral.

theorem QFT.gff_complex_CF_covariance (m : ℝ) [Fact (0 < m)] (f : TestFunctionℂ) : GJGeneratingFunctionalℂ (muGFF m) f = Complex.exp (-(1 / 2) * freeCovarianceℂBilinear m f f)

The complex characteristic functional of the GFF.

For any complex test function f: Z[f] = E[exp(i⟨ω,f⟩_ℂ)] = exp(-½ C_ℂ(f, f))

Proved by 1-parameter analytic continuation: decompose f = f_re + I·f_im, show the generating functional and Gaussian formula agree on ℝ (from gff_real_characteristic), extend to ℂ via the identity theorem.

Bilinear Expansion for Finite Sums

Using the ℂ-bilinearity of freeCovarianceℂBilinear, we expand C_ℂ(∑ᵢ zᵢ Jᵢ, ∑ⱼ zⱼ Jⱼ) = ∑ᵢ ∑ⱼ zᵢ zⱼ C_ℂ(Jᵢ, Jⱼ).

theorem QFT.freeCovarianceℂ_bilinear_sum_expansion (m : ℝ) [Fact (0 < m)] {n : ℕ} (J : Fin n → TestFunctionℂ) (z : Fin n → ℂ) : freeCovarianceℂBilinear m (∑ i : Fin n, z i • J i) (∑ j : Fin n, z j • J j) = ∑ i : Fin n, ∑ j : Fin n, z i * z j * freeCovarianceℂBilinear m (J i) (J j)

Full bilinear expansion of C_ℂ(∑ zᵢ Jᵢ, ∑ zⱼ Jⱼ) as a finite double sum.

theorem QFT.gff_generating_eq_exp_quadratic (m : ℝ) [Fact (0 < m)] {n : ℕ} (J : Fin n → TestFunctionℂ) (z : Fin n → ℂ) : GJGeneratingFunctionalℂ (muGFF m) (∑ i : Fin n, z i • J i) = Complex.exp (-(1 / 2) * ∑ i : Fin n, ∑ j : Fin n, z i * z j * freeCovarianceℂBilinear m (J i) (J j))

The generating functional for ∑ᵢ zᵢ Jᵢ equals exp of a finite quadratic form.

Analyticity of exp(finite quadratic form)

A finite quadratic form z ↦ ∑ᵢⱼ Aᵢⱼ zᵢ zⱼ is a polynomial, hence analytic. Composing with exp preserves analyticity.

theorem QFT.analyticOn_finite_quadratic {n : ℕ} (A : Fin n → Fin n → ℂ) : AnalyticOn ℂ (fun (z : Fin n → ℂ) => ∑ i : Fin n, ∑ j : Fin n, z i * z j * A i j) Set.univ

A finite quadratic form ∑ᵢⱼ Aᵢⱼ zᵢ zⱼ is analytic (it's a polynomial).

theorem QFT.gaussianFreeField_satisfies_OS0 (m : ℝ) [Fact (0 < m)] : os0Analyticity (muGFF m)

The Gaussian Free Field satisfies the OS0 Analyticity axiom.

Direct proof from the covariance structure: Z[f] = exp(-½ C_ℂ(f,f)) and C_ℂ is ℂ-bilinear, so Z[∑ zᵢ Jᵢ] = exp(quadratic polynomial in z).