# `TwoPoint.lean` — Informal Summary

> **Source**: [`OSforGFF/Schwinger/TwoPoint.lean`](../../OSforGFF/Schwinger/TwoPoint.lean)
> **Generated**: 2026-03-03 12:38
> **Note**: Auto-generated by `/lean-summarize`. Re-run to refresh.

## Overview

Defines the two-point Schwinger function $S_2(x) = \langle\phi(x)\phi(0)\rangle$ as the
limit of smeared correlations as the smearing mollifiers shrink to Dirac deltas.
For a bump function sequence $\phi_\varepsilon$ with outer radius $\varepsilon \to 0$,
$S_2(x) := \lim_{\varepsilon\to 0} S_2(\phi_\varepsilon(\cdot - x), \phi_\varepsilon)$.
The main theorem `schwingerTwoPointFunction_eq_kernel` shows that for any measure
whose two-point Schwinger function computes as a double integral against a continuous
kernel $C$, the limit-based definition recovers $C(x)$ for $x \neq 0$.

## Status

**Main result**: Fully proven

**Major gaps**: None — file is sorry-free.

**Length**: 231 lines, 5 definition(s) + 4 theorem(s)/lemma(s)

---

## Two-Point Schwinger Function Infrastructure

### [`bumpToSchwartz`](../../OSforGFF/Schwinger/TwoPoint.lean#L45) — Definition

**Lean signature**
```lean
noncomputable def bumpToSchwartz (φ : ContDiffBump (0 : SpaceTime)) : TestFunction
```
**Informal**: Converts a compactly supported smooth bump function $\phi$ centered at $0$ into a (real-valued) Schwartz test function by using its $L^1$-normalized version $\phi/\lVert\phi\rVert_1$.

---

### [`bumpToSchwartz_apply`](../../OSforGFF/Schwinger/TwoPoint.lean#L51) — Theorem

**Statement**: `bumpToSchwartz φ x = φ.normed volume x`, i.e., the Schwartz function produced by `bumpToSchwartz` evaluates pointwise to the $L^1$-normalized bump.

**Proof uses**: *(direct tactic proof)*

---

### [`translateSchwartz`](../../OSforGFF/Schwinger/TwoPoint.lean#L59) — Definition

**Lean signature**
```lean
noncomputable def translateSchwartz (f : TestFunction) (a : SpaceTime) : TestFunction
```
**Informal**: The translate of a Schwartz test function $f$ by a vector $a \in \mathbb{R}^4$, defined as $(\tau_a f)(x) = f(x - a)$; an alias for `SchwartzMap.translate`.

---

### [`SmearedTwoPointFunction`](../../OSforGFF/Schwinger/TwoPoint.lean#L67) — Definition

**Lean signature**
```lean
noncomputable def SmearedTwoPointFunction (dμ_config : ProbabilityMeasure FieldConfiguration)
    (φ : ContDiffBump (0 : SpaceTime)) (x : SpaceTime) : ℝ
```
**Informal**: The smeared two-point correlation function
$\int\!\int \phi(u-x)\,\langle\phi(u)\phi(v)\rangle_\mu\,\phi(v)\,du\,dv$,
obtained by evaluating the two-point Schwinger function $S_2$ on the translated and untranslated normalized bumps.

---

### [`standardBumpSequence`](../../OSforGFF/Schwinger/TwoPoint.lean#L75) — Definition

**Lean signature**
```lean
noncomputable def standardBumpSequence (n : ℕ) (hn : n ≠ 0) : ContDiffBump (0 : SpaceTime)
```
**Informal**: The canonical sequence of bump functions with outer radius $r_{\mathrm{out}} = 1/n$ and inner radius $r_{\mathrm{in}} = 1/(2n)$, used to define the limit $S_2(x) = \lim_{n\to\infty}\text{SmearedTwoPointFunction}(\phi_{1/n}, x)$.

---

### [`SchwingerTwoPointFunction`](../../OSforGFF/Schwinger/TwoPoint.lean#L102) — Definition

**Lean signature**
```lean
noncomputable def SchwingerTwoPointFunction
    (dμ_config : ProbabilityMeasure FieldConfiguration) (x : SpaceTime) : ℝ
```
**Informal**: The two-point Schwinger function $S_2(x)$, defined as $0$ at the coincident point $x = 0$ (regularization) and otherwise as $\lim_{n\to\infty} \text{SmearedTwoPointFunction}(\phi_{1/n}, x)$ along the standard bump sequence.

---

### [`schwingerTwoPointFunction_zero`](../../OSforGFF/Schwinger/TwoPoint.lean#L114) — Theorem

**Statement**: The two-point Schwinger function vanishes at coincident points: $S_2(0) = 0$.

**Proof uses**: *(direct tactic proof)*

---

### [`smearedTwoPoint_tendsto_schwingerTwoPoint`](../../OSforGFF/Schwinger/TwoPoint.lean#L131) — Theorem

**Statement**: For any net of bump functions $\phi_i$ with $r_{\mathrm{out},i} \to 0$, if the two-point Schwinger function is given by integration against a continuous kernel $C$ (continuous away from $0$), then the smeared two-point functions converge to $C(x)$ for $x \neq 0$:
$$\text{SmearedTwoPointFunction}(\phi_i, x) \xrightarrow{i} C(x).$$

**Proof uses**: [`double_mollifier_convergence`](../../OSforGFF/General/FunctionalAnalysis.lean#L991), [`bumpToSchwartz_apply`](../../OSforGFF/Schwinger/TwoPoint.lean#L51), [`translateSchwartz`](../../OSforGFF/Schwinger/TwoPoint.lean#L59), [`SchwartzMap.translate`](../../OSforGFF/General/FunctionalAnalysis.lean#L804)

---

### [`schwingerTwoPointFunction_eq_kernel`](../../OSforGFF/Schwinger/TwoPoint.lean#L167) — Theorem

**Statement**: For $x \neq 0$, if the measure $\mu$ has a two-point Schwinger function of the form $S_2(f,g) = \int\!\int f(u)\,C(u-v)\,g(v)\,du\,dv$ for a kernel $C$ continuous away from $0$, then the limit-based definition recovers the kernel:
$\text{SchwingerTwoPointFunction}_\mu(x) = C(x)$.

**Proof uses**: [`smearedTwoPoint_tendsto_schwingerTwoPoint`](../../OSforGFF/Schwinger/TwoPoint.lean#L131), [`standardBumpSequence`](../../OSforGFF/Schwinger/TwoPoint.lean#L75), `tendsto_one_div_add_atTop_nhds_zero_nat`, `Filter.Tendsto.limUnder_eq`, `tendsto_of_tendsto_succ`

---

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