# `Wick.lean` -- Informal Summary

> **Source**: [`GaussianField/Wick.lean`](../../GaussianField/Wick.lean)
> **Generated**: 2026-03-03 11:30
> **Note**: Auto-generated by `/lean-summarize`. Re-run to refresh.

## Overview

Proves Wick's theorem (Isserlis' theorem) for centered Gaussian measures in both recursive and bound forms. The key analytic input is Gaussian integration by parts, derived by differentiating the characteristic functional in two ways (Leibniz integral rule vs. chain rule on the closed-form expression). The recursive form avoids enumerating perfect pairings; the bound form gives $\lvert E[\prod \omega(f_i)] \rvert \le (n-1)!! \cdot \prod \lVert Tf_i \rVert$, sufficient for verifying the OS1' Schwinger function growth condition.

## Status

**Main result**: Fully proven

None -- file is sorry-free.

**Length**: 1067 lines, 0 definition(s) + 11 theorem(s)/lemma(s)

---

## Integrability of products

### [`product_integrable`](../../GaussianField/Wick.lean#L106) -- Theorem

**Statement**: Finite products of evaluation functionals $\prod_i \omega(f_i)$ are integrable under the Gaussian measure.

**Proof uses**: [`pairing_memLp`](../../GaussianField/Properties.lean), `MemLp.mul'`, `ENNReal.HolderTriple`

---

## Gaussian integration by parts

### [`gaussian_ibp`](../../GaussianField/Wick.lean#L240) -- Theorem

**Statement**: Gaussian integration by parts:
$$\int \omega(f_0)\,e^{i\,\omega(h)}\,d\mu = \langle Tf_0, Th \rangle \cdot i \cdot \int e^{i\,\omega(h)}\,d\mu.$$

**Proof uses**: `hasDerivAt_charFun_closed`, `hasDerivAt_charFun_leibniz`, `HasDerivAt.unique`, [`charFun`](../../GaussianField/Construction.lean)

---

## Generalized Gaussian IBP

### [`gaussian_ibp_general`](../../GaussianField/Wick.lean#L475) -- Theorem

**Statement**: Generalized Gaussian IBP for polynomial times exponential functionals:
$$E\Bigl[\omega(f_0)\prod_i \omega(g_i)\,e^{i\omega(h)}\Bigr] = \sum_j C(f_0, g_j)\,E\Bigl[\prod_{i \ne j}\omega(g_i)\,e^{i\omega(h)}\Bigr] + C(f_0, h)\cdot i\cdot E\Bigl[\prod_i \omega(g_i)\,e^{i\omega(h)}\Bigr]$$
where $C(f,g) = \langle Tf, Tg \rangle$.

**Proof uses**: [`gaussian_ibp`](../../GaussianField/Wick.lean#L240), `hasDerivAt_weighted_exp_leibniz`, `HasDerivAt.unique`, [`product_integrable`](../../GaussianField/Wick.lean#L106)

---

## Wick's theorem -- recursive form

### [`wick_recursive`](../../GaussianField/Wick.lean#L846) -- Theorem

**Statement**: **Wick's theorem (recursive form)**: for a centered Gaussian with covariance $C(f,g) = \langle Tf, Tg \rangle_H$:
$$E\bigl[\omega(f_0)\prod_j \omega(g_j)\bigr] = \sum_j C(f_0, g_j)\,E\Bigl[\prod_{i \ne j}\omega(g_i)\Bigr].$$

**Proof uses**: [`gaussian_ibp_general`](../../GaussianField/Wick.lean#L475), [`cross_moment_eq_covariance`](../../GaussianField/Properties.lean), [`product_integrable`](../../GaussianField/Wick.lean#L106), `Complex.ofRealCLM.integral_comp_comm`

---

## Odd moments vanish

### [`odd_moment_vanish`](../../GaussianField/Wick.lean#L905) -- Theorem

**Statement**: All odd-order moments of a centered Gaussian measure vanish: $E[\prod_{i=0}^{2k} \omega(f_i)] = 0$.

**Proof uses**: [`wick_recursive`](../../GaussianField/Wick.lean#L846), [`measure_centered`](../../GaussianField/Properties.lean)

---

## Wick bound

### [`wick_bound`](../../GaussianField/Wick.lean#L945) -- Theorem

**Statement**: **Wick bound on $n$-point functions**:
$$\bigl\lVert E\bigl[\prod_i \omega(f_i)\bigr] \bigr\rVert \le (n-1)!!\cdot \prod_i \lVert T(f_i) \rVert.$$

**Proof uses**: [`wick_recursive`](../../GaussianField/Wick.lean#L846), [`odd_moment_vanish`](../../GaussianField/Wick.lean#L905), [`measure_centered`](../../GaussianField/Properties.lean), `norm_inner_le_norm`, `norm_sum_le`

---

## OS1' Schwinger growth for GFF

### [`double_factorial_le_sqrt_factorial`](../../GaussianField/Wick.lean#L1033) -- Theorem

**Statement**: $(n-1)!! \le \sqrt{n!}$ for all $n$. This converts the Wick bound into the OS1' factorial form.

**Proof uses**: `dfact_sq_le_succ_fact`, `Real.le_sqrt`

---

### [`wick_bound_factorial`](../../GaussianField/Wick.lean#L1058) -- Theorem

**Statement**: Wick bound in factorial form (suitable for OS1'):
$$\bigl\lVert E\bigl[\prod_i \omega(f_i)\bigr] \bigr\rVert \le \sqrt{n!}\cdot \prod_i \lVert T(f_i) \rVert.$$

**Proof uses**: [`wick_bound`](../../GaussianField/Wick.lean#L945), [`double_factorial_le_sqrt_factorial`](../../GaussianField/Wick.lean#L1033)

---

*This file has **0** definitions and **11** theorems/lemmas (0 with sorry).*