# `OS4_MGF.lean` — Informal Summary

> **Source**: [`OSforGFF/OS/OS4_MGF.lean`](../../OSforGFF/OS/OS4_MGF.lean)
> **Generated**: 2026-03-03 00:00
> **Note**: Auto-generated by `/lean-summarize`. Re-run to refresh.

## Overview

Provides shared infrastructure for the OS4 clustering and ergodicity proofs.
The key ingredients are: (1) the duality identity
$\langle T_s \omega, g \rangle = \langle \omega, T_{-s} g \rangle$
for time-translated distributions; (2) the GFF moment generating function (MGF)
formula $\mathbb{E}[e^{\langle \omega, J \rangle}] = e^{\frac{1}{2}C(J,J)}$
and its time-translation invariance; (3) joint MGF factorization
$\mathbb{E}[e^{\langle\omega,f\rangle+\langle\omega,g\rangle}]
= \mathbb{E}[e^{\langle\omega,f\rangle}]\,\mathbb{E}[e^{\langle\omega,g\rangle}]\,
e^{S_2(f,g)}$; and (4) the exponential bound
$\lVert e^z - 1 \rVert \leq \lVert z \rVert e^{\lVert z \rVert}$.

## Status

**Main result**: Fully proven (0 sorries)

None — file is sorry-free.

**Length**: 276 lines, 1 definition + 10 lemmas

---

## Time Translation Infrastructure

### [`timeTranslationSchwartzℂ_decompose_fst`](../../OSforGFF/OS/OS4_MGF.lean#L77) — Lemma

**Statement**: Time translation commutes with real-part extraction: the real part of
$T_s g$ (as a complex Schwartz function) equals $T_s$ applied to the real part of $g$.

**Proof uses**: `complex_testfunction_decompose_fst_apply`, `timeTranslationSchwartz_apply`,
`timeTranslationSchwartzℂ_apply`

---

### [`timeTranslationSchwartzℂ_decompose_snd`](../../OSforGFF/OS/OS4_MGF.lean#L85) — Lemma

**Statement**: Time translation commutes with imaginary-part extraction: the imaginary
part of $T_s g$ equals $T_s$ applied to the imaginary part of $g$.

**Proof uses**: `complex_testfunction_decompose_snd_apply`, `timeTranslationSchwartz_apply`,
`timeTranslationSchwartzℂ_apply`

---

### [`timeTranslationDistribution_pairingℂ`](../../OSforGFF/OS/OS4_MGF.lean#L94) — Lemma

**Statement**: Time translation on distributions is dual to time translation on test
functions:
$$\langle T_s \omega, g \rangle_{\mathbb{C}} = \langle \omega, T_{-s} g \rangle_{\mathbb{C}}.$$

**Proof uses**: [`timeTranslationSchwartzℂ_decompose_fst`](../../OSforGFF/OS/OS4_MGF.lean#L77),
[`timeTranslationSchwartzℂ_decompose_snd`](../../OSforGFF/OS/OS4_MGF.lean#L85),
`timeTranslationDistribution_apply`

---

### [`continuous_distributionPairingℂ_timeTranslation`](../../OSforGFF/OS/OS4_MGF.lean#L111) — Lemma

**Statement**: The map $s \mapsto \langle T_s \omega, g \rangle_{\mathbb{C}}$ is
continuous in $s$.

**Proof uses**: [`timeTranslationDistribution_pairingℂ`](../../OSforGFF/OS/OS4_MGF.lean#L94),
[`timeTranslationSchwartzℂ_decompose_fst`](../../OSforGFF/OS/OS4_MGF.lean#L77),
[`timeTranslationSchwartzℂ_decompose_snd`](../../OSforGFF/OS/OS4_MGF.lean#L85),
`continuous_timeTranslationSchwartz`

---

## Euclidean Group Infrastructure for Time Translation

### `timeTranslationE` — Definition

**Lean signature**
```lean
def timeTranslationE (t : ℝ) : QFT.E
```
**Informal**: The Euclidean group element corresponding to time translation by $t$,
given by the pair (identity rotation, $-t$) in $O(4) \ltimes \mathbb{R}^4$.

---

### [`euclidean_action_timeTranslationE`](../../OSforGFF/OS/OS4_MGF.lean#L145) — Lemma

**Statement**: The Euclidean group action of `timeTranslationE t` on a test function $f$
coincides with the time-translation Schwartz map $T_t f$.

**Proof uses**: `QFT.euclidean_action_apply`, `timeTranslationSchwartzℂ_apply`,
`timeShift_eq_add_const`

---

## GFF Covariance Invariance

### [`freeCovarianceℂ_bilinear_timeTranslation_invariant`](../../OSforGFF/OS/OS4_MGF.lean#L161) — Lemma

**Statement**: The GFF complex covariance bilinear form is invariant under simultaneous
time translation of both arguments:
$$C(T_t f, T_t g) = C(f, g).$$

**Proof uses**: [`euclidean_action_timeTranslationE`](../../OSforGFF/OS/OS4_MGF.lean#L145),
[`freeCovarianceℂ_bilinear_euclidean_invariant`](../../OSforGFF/OS/OS2_Invariance.lean#L106)

---

## GFF Moment Generating Function

### [`gff_mgf_formula`](../../OSforGFF/OS/OS4_MGF.lean#L172) — Lemma

**Statement**: The GFF moment generating function satisfies
$$\mathbb{E}\bigl[e^{\langle\omega, J\rangle}\bigr]
= e^{\frac{1}{2} C(J, J)},$$
where $C(J, J) = \int\!\int \bar J(x)\, C(x,y)\, J(y)\, dx\, dy$ is the complex
covariance bilinear form.

**Proof uses**: [`GFFIsGaussian.gff_complex_characteristic_OS0`](../../OSforGFF/Measure/IsGaussian.lean#L221),
[`freeCovarianceℂ_bilinear_smul_left`](../../OSforGFF/Covariance/Position.lean#L505),
[`freeCovarianceℂ_bilinear_smul_right`](../../OSforGFF/Covariance/Position.lean#L556),
`pairing_linear_combo`

---

### [`gff_generating_time_invariant`](../../OSforGFF/OS/OS4_MGF.lean#L203) — Lemma

**Statement**: The GFF generating functional is invariant under time translation of the
source:
$$\mathbb{E}\bigl[e^{\langle\omega, T_s f\rangle}\bigr]
= \mathbb{E}\bigl[e^{\langle\omega, f\rangle}\bigr].$$

**Proof uses**: [`gff_mgf_formula`](../../OSforGFF/OS/OS4_MGF.lean#L172),
[`freeCovarianceℂ_bilinear_timeTranslation_invariant`](../../OSforGFF/OS/OS4_MGF.lean#L161)

---

## Joint MGF Factorization

### [`gff_joint_mgf_factorization`](../../OSforGFF/OS/OS4_MGF.lean#L216) — Lemma

**Statement**: The GFF joint moment generating functional factorizes as
$$\mathbb{E}\bigl[e^{\langle\omega,f\rangle + \langle\omega,g\rangle}\bigr]
= \mathbb{E}\bigl[e^{\langle\omega,f\rangle}\bigr]\,
  \mathbb{E}\bigl[e^{\langle\omega,g\rangle}\bigr]\,
  e^{S_2(f,g)},$$
where $S_2(f,g)$ is the two-point Schwinger function of the GFF.

**Proof uses**: [`gff_mgf_formula`](../../OSforGFF/OS/OS4_MGF.lean#L172),
[`gff_two_point_equals_covarianceℂ_free`](../../OSforGFF/Measure/IsGaussian.lean#L463),
[`freeCovarianceℂ_bilinear_add_left`](../../OSforGFF/Covariance/Position.lean#L495),
[`freeCovarianceℂ_bilinear_add_right`](../../OSforGFF/Covariance/Position.lean#L567),
[`freeCovarianceℂ_bilinear_symm`](../../OSforGFF/Covariance/Position.lean#L528),
`pairing_linear_combo`

---

## Exponential Bound

### [`exp_sub_one_bound_general`](../../OSforGFF/OS/OS4_MGF.lean#L248) — Lemma

**Statement**: For any complex $x$,
$$\lVert e^x - 1 \rVert \leq \lVert x \rVert \cdot e^{\lVert x \rVert}.$$

**Proof uses**: `Complex.norm_exp_sub_sum_le_exp_norm_sub_sum`, `Real.add_one_le_exp`

---

*This file has **1** definition and **10** lemmas (0 with sorry).*