# `RealForm.lean` — Informal Summary

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

## Overview

This file provides the real covariance bilinear form $C_{\mathbb{R}}(f,g) = \iint f(x)\,C(x,y)\,g(y)\,dx\,dy$ for real Schwartz test functions, and proves that it is realised as a squared Hilbert-space norm via the `sqrtPropagatorEmbedding` theorem. The embedding map $T : \mathcal{D} \to L^2$ sends $f$ to $\hat f(k)\cdot(\lVert k\rVert^2+m^2)^{-1/2}$ in momentum space, and the key identity $C_{\mathbb{R}}(f,f) = \lVert Tf\rVert^2$ follows from the Parseval identity. Additional results establish continuity, positivity, bilinearity, symmetry, and time-reflection invariance of the quadratic form.

## Status

**Main result**: Fully proven (zero sorries).

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

**Length**: 741 lines, 10 definition(s) + 26 theorem(s)/lemma(s)

---

## Real Covariance Form

### `freeCovarianceFormR` — Definition

**Lean signature**
```lean
noncomputable def freeCovarianceFormR (m : ℝ) (f g : TestFunction) : ℝ
```
**Informal**: The real-valued covariance bilinear form $C_{\mathbb{R}}(f,g) = \iint f(x)\,C(x,y)\,g(y)\,dx\,dy$ on real Schwartz test functions.

---

### [`freeCovarianceℂ_bilinear_agrees_on_reals`](../../OSforGFF/Covariance/RealForm.lean#L50) — Theorem

**Statement**: For real test functions $f, g$, the complex bilinear form evaluated at their complexifications equals the real form cast to $\mathbb{C}$: $\langle f_{\mathbb{C}}, g_{\mathbb{C}}\rangle_{C,\mathbb{C}} = (C_{\mathbb{R}}(f,g) : \mathbb{C})$.

**Proof uses**: `integral_ofReal`

---

## Weighted L² Space Construction

### `momentumWeightMeasure` — Definition

**Lean signature**
```lean
noncomputable def momentumWeightMeasure (m : ℝ) : Measure SpaceTime
```
**Informal**: The weighted measure on momentum space with density $(\lVert k\rVert^2+m^2)^{-1}$ with respect to Lebesgue measure.

---

### `fourierTransformCLM_real` — Definition

**Lean signature**
```lean
noncomputable def fourierTransformCLM_real : TestFunctionℂ →L[ℝ] TestFunctionℂ
```
**Informal**: The $\mathbb{R}$-linear restriction of the complex Schwartz-space Fourier transform $\mathcal{F} : \mathcal{S}\to\mathcal{S}$.

---

### `schwartzToL2CLM_real` — Definition

**Lean signature**
```lean
noncomputable def schwartzToL2CLM_real (_m : ℝ) : TestFunctionℂ →L[ℝ] Lp ℂ 2 (volume : Measure SpaceTime)
```
**Informal**: The $\mathbb{R}$-linear restriction of the Schwartz-to-$L^2$ continuous inclusion map.

---

## The Embedding Map

### `sqrtPropagatorMap` — Definition

**Lean signature**
```lean
noncomputable def sqrtPropagatorMap (m : ℝ) (f : TestFunction) : SpaceTime → ℂ
```
**Informal**: The embedding $T f(k) = \hat f_{\mathbb{C}}(k)\cdot(\lVert k\rVert^2+m^2)^{-1/2}$ in momentum space, where $\hat f_{\mathbb{C}}$ is the Fourier transform and the weight uses the Mathlib normalisation convention.

---

### [`sqrtPropagatorMap_sq_integrable`](../../OSforGFF/Covariance/RealForm.lean#L95) — Lemma

**Statement**: For $m>0$, the squared pointwise norm $\lVert Tf(k)\rVert^2$ is integrable over momentum space.

**Proof uses**: [`schwartz_L2_integrable`](../../OSforGFF/Covariance/Momentum.lean#L70), [`momentumWeightSqrt_mathlib_le_inv_mass`](../../OSforGFF/Covariance/Momentum.lean#L2313), [`momentumWeightSqrt_mathlib_pos`](../../OSforGFF/Covariance/Momentum.lean#L2168)

---

### [`sqrtPropagatorMap_memLp`](../../OSforGFF/Covariance/RealForm.lean#L149) — Lemma

**Statement**: For $m>0$, the embedded function $Tf$ lies in $L^2(\mathbb{R}^4)$.

**Proof uses**: [`sqrtPropagatorMap_sq_integrable`](../../OSforGFF/Covariance/RealForm.lean#L95), `memLp_two_iff_integrable_sq_norm`

---

### `sqrtPropagatorMap_norm_sq` — Definition

**Lean signature**
```lean
noncomputable def sqrtPropagatorMap_norm_sq (m : ℝ) (f : TestFunction) : ℝ
```
**Informal**: The squared $L^2$-norm $\lVert Tf\rVert^2 = \int \lVert Tf(k)\rVert^2\,dk$ of the embedded function.

---

### [`sqrtPropagatorMap_linear_add`](../../OSforGFF/Covariance/RealForm.lean#L172) — Lemma

**Statement**: The embedding map is additive: $T(f+g) = Tf + Tg$.

**Proof uses**: `toComplex_add`

---

### [`sqrtPropagatorMap_linear_smul`](../../OSforGFF/Covariance/RealForm.lean#L180) — Lemma

**Statement**: The embedding map is $\mathbb{R}$-homogeneous: $T(c\cdot f) = c\cdot Tf$.

**Proof uses**: `toComplex_smul`

---

## Connection to Covariance

### [`toComplex_star`](../../OSforGFF/Covariance/RealForm.lean#L190) — Lemma

**Statement**: For a real test function $f$, the complex conjugate of $f_{\mathbb{C}}(x)$ equals $f_{\mathbb{C}}(x)$ (real-valued functions are self-conjugate).

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

---

### [`freeCovarianceℂ_eq_bilinear_on_reals`](../../OSforGFF/Covariance/RealForm.lean#L195) — Lemma

**Statement**: For real test functions, the two complex bilinear forms agree: $\langle f_{\mathbb{C}}, g_{\mathbb{C}}\rangle_{C,\mathbb{C}} = \langle f_{\mathbb{C}}, g_{\mathbb{C}}\rangle_{C,\mathrm{bil}}$.

**Proof uses**: [`toComplex_star`](../../OSforGFF/Covariance/RealForm.lean#L190)

---

### [`sqrtPropagatorMap_norm_eq_covariance`](../../OSforGFF/Covariance/RealForm.lean#L204) — Lemma

**Statement**: The squared $L^2$-norm of the embedding equals the real covariance form: $\lVert Tf\rVert^2 = C_{\mathbb{R}}(f,f)$.

**Proof uses**: [`momentumWeightSqrt_mathlib_sq`](../../OSforGFF/Covariance/Momentum.lean#L2179), [`parseval_covariance_schwartz_bessel`](../../OSforGFF/Covariance/Position.lean#L628), [`freeCovarianceℂ_eq_bilinear_on_reals`](../../OSforGFF/Covariance/RealForm.lean#L195), [`freeCovarianceℂ_bilinear_agrees_on_reals`](../../OSforGFF/Covariance/RealForm.lean#L50)

---

## The Proof of sqrtPropagatorEmbedding

### `TargetHilbertSpace` — Definition (abbrev)

**Lean signature**
```lean
abbrev TargetHilbertSpace (_m : ℝ) : Type
```
**Informal**: The target Hilbert space for the embedding, namely $L^2(\mathbb{R}^4;\mathbb{C})$ with the Lebesgue measure.

---

### `embeddingMap` — Definition

**Lean signature**
```lean
noncomputable def embeddingMap (m : ℝ) [Fact (0 < m)] : TestFunction →ₗ[ℝ] TargetHilbertSpace m
```
**Informal**: The $\mathbb{R}$-linear map $T : \mathcal{D} \to L^2$ sending $f$ to its $L^2$ representative $Tf$, constructed from `sqrtPropagatorMap_memLp`.

---

### `embeddingMapCLM` — Definition

**Lean signature**
```lean
noncomputable def embeddingMapCLM (m : ℝ) [Fact (0 < m)] : TestFunction →L[ℝ] Lp ℂ 2 (volume : Measure SpaceTime)
```
**Informal**: A continuous linear map form of the embedding, built by composing the Fourier transform, the Schwartz-to-$L^2$ map, and multiplication by the square-root weight.

---

### [`embeddingMapCLM_apply`](../../OSforGFF/Covariance/RealForm.lean#L302) — Lemma

**Statement**: The continuous linear map `embeddingMapCLM` agrees with the algebraically-defined `embeddingMap` on all test functions.

**Proof uses**: [`momentumWeightSqrt_mathlib_mul_CLM_spec`](../../OSforGFF/Covariance/Momentum.lean#L2305), [`sqrtPropagatorMap_memLp`](../../OSforGFF/Covariance/RealForm.lean#L149)

---

### [`sqrtPropagatorEmbedding`](../../OSforGFF/Covariance/RealForm.lean#L341) — Theorem

**Statement**: There exists a Hilbert space $H$, a continuous inner-product space structure on $H$, and an $\mathbb{R}$-linear map $T : \mathcal{D} \to H$ such that $C_{\mathbb{R}}(f,f) = \lVert Tf\rVert^2$ for all test functions $f$.

**Proof uses**: [`sqrtPropagatorMap_norm_eq_covariance`](../../OSforGFF/Covariance/RealForm.lean#L204), [`sqrtPropagatorMap_memLp`](../../OSforGFF/Covariance/RealForm.lean#L149), [`sqrtPropagatorMap_sq_integrable`](../../OSforGFF/Covariance/RealForm.lean#L95)

---

## Auxiliary Lemmas for Continuity

### [`embeddingMap_norm_sq`](../../OSforGFF/Covariance/RealForm.lean#L388) — Lemma

**Statement**: $\lVert Tf\rVert^2 = \int \lVert Tf(k)\rVert^2\,dk$ (expressing the $L^2$-norm via the pointwise integral).

**Proof uses**: [`sqrtPropagatorMap_memLp`](../../OSforGFF/Covariance/RealForm.lean#L149), [`sqrtPropagatorMap_sq_integrable`](../../OSforGFF/Covariance/RealForm.lean#L95)

---

### [`freeCovarianceFormR_eq_normSq`](../../OSforGFF/Covariance/RealForm.lean#L431) — Lemma

**Statement**: $C_{\mathbb{R}}(f,f) = \lVert Tf\rVert^2$ (combining the covariance-norm identity with the $L^2$-norm formula).

**Proof uses**: [`sqrtPropagatorMap_norm_eq_covariance`](../../OSforGFF/Covariance/RealForm.lean#L204), [`embeddingMap_norm_sq`](../../OSforGFF/Covariance/RealForm.lean#L388)

---

### [`embeddingMap_continuous`](../../OSforGFF/Covariance/RealForm.lean#L438) — Lemma

**Statement**: The embedding map $T : \mathcal{D} \to L^2$ is continuous.

**Proof uses**: [`embeddingMapCLM`](../../OSforGFF/Covariance/RealForm.lean#L297), [`embeddingMapCLM_apply`](../../OSforGFF/Covariance/RealForm.lean#L302)

---

## Positivity and Other Properties

### [`freeCovarianceFormR_continuous`](../../OSforGFF/Covariance/RealForm.lean#L449) — Theorem

**Statement**: The real quadratic form $f \mapsto C_{\mathbb{R}}(f,f)$ is continuous on the Schwartz space of real test functions.

**Proof uses**: [`freeCovarianceFormR_eq_normSq`](../../OSforGFF/Covariance/RealForm.lean#L431), [`embeddingMap_continuous`](../../OSforGFF/Covariance/RealForm.lean#L438)

---

### [`freeCovarianceFormR_pos`](../../OSforGFF/Covariance/RealForm.lean#L462) — Theorem

**Statement**: The real covariance quadratic form is non-negative: $C_{\mathbb{R}}(f,f) \ge 0$ for all real test functions $f$.

**Proof uses**: [`freeCovarianceℂ_bilinear_agrees_on_reals`](../../OSforGFF/Covariance/RealForm.lean#L50), [`freeCovarianceℂ_eq_bilinear_on_reals`](../../OSforGFF/Covariance/RealForm.lean#L195), [`freeCovarianceℂ_positive`](../../OSforGFF/Covariance/Position.lean#L601)

---

### [`freeCovarianceFormR_symm`](../../OSforGFF/Covariance/RealForm.lean#L476) — Theorem

**Statement**: The real covariance bilinear form is symmetric: $C_{\mathbb{R}}(f,g) = C_{\mathbb{R}}(g,f)$.

**Proof uses**: [`freeCovarianceℂ_bilinear_agrees_on_reals`](../../OSforGFF/Covariance/RealForm.lean#L50), [`freeCovarianceℂ_bilinear_symm`](../../OSforGFF/Covariance/Position.lean#L528)

---

### [`freeCovarianceFormR_add_left`](../../OSforGFF/Covariance/RealForm.lean#L488) — Lemma

**Statement**: $C_{\mathbb{R}}(f_1+f_2,g) = C_{\mathbb{R}}(f_1,g) + C_{\mathbb{R}}(f_2,g)$.

**Proof uses**: [`freeCovarianceℂ_bilinear_add_left`](../../OSforGFF/Covariance/Position.lean#L495), [`freeCovarianceℂ_bilinear_agrees_on_reals`](../../OSforGFF/Covariance/RealForm.lean#L50)

---

### [`freeCovarianceFormR_smul_left`](../../OSforGFF/Covariance/RealForm.lean#L512) — Lemma

**Statement**: $C_{\mathbb{R}}(c\cdot f,g) = c\cdot C_{\mathbb{R}}(f,g)$.

**Proof uses**: [`freeCovarianceℂ_bilinear_smul_left`](../../OSforGFF/Covariance/Position.lean#L505), [`freeCovarianceℂ_bilinear_agrees_on_reals`](../../OSforGFF/Covariance/RealForm.lean#L50)

---

### [`freeCovarianceFormR_add_right`](../../OSforGFF/Covariance/RealForm.lean#L538) — Lemma

**Statement**: $C_{\mathbb{R}}(f,g_1+g_2) = C_{\mathbb{R}}(f,g_1) + C_{\mathbb{R}}(f,g_2)$.

**Proof uses**: [`freeCovarianceℂ_bilinear_add_right`](../../OSforGFF/Covariance/Position.lean#L567), [`freeCovarianceℂ_bilinear_agrees_on_reals`](../../OSforGFF/Covariance/RealForm.lean#L50)

---

### [`freeCovarianceFormR_smul_right`](../../OSforGFF/Covariance/RealForm.lean#L562) — Lemma

**Statement**: $C_{\mathbb{R}}(f,c\cdot g) = c\cdot C_{\mathbb{R}}(f,g)$.

**Proof uses**: [`freeCovarianceℂ_bilinear_smul_right`](../../OSforGFF/Covariance/Position.lean#L556), [`freeCovarianceℂ_bilinear_agrees_on_reals`](../../OSforGFF/Covariance/RealForm.lean#L50)

---

### [`freeCovarianceFormR_zero_left`](../../OSforGFF/Covariance/RealForm.lean#L588) — Lemma

**Statement**: $C_{\mathbb{R}}(0,g) = 0$.

**Proof uses**: [`freeCovarianceFormR_smul_left`](../../OSforGFF/Covariance/RealForm.lean#L512)

---

### [`freeCovarianceFormR_zero_right`](../../OSforGFF/Covariance/RealForm.lean#L596) — Lemma

**Statement**: $C_{\mathbb{R}}(f,0) = 0$.

**Proof uses**: [`freeCovarianceFormR_symm`](../../OSforGFF/Covariance/RealForm.lean#L476), [`freeCovarianceFormR_zero_left`](../../OSforGFF/Covariance/RealForm.lean#L588)

---

### [`freeCovarianceFormR_reflection_invariant`](../../OSforGFF/Covariance/RealForm.lean#L601) — Lemma

**Statement**: The real covariance form is invariant under time reflection in both arguments: $C_{\mathbb{R}}(\Theta_{\mathbb{R}} f, \Theta_{\mathbb{R}} g) = C_{\mathbb{R}}(f,g)$.

**Proof uses**: [`freeCovarianceℂ_bilinear_integrable`](../../OSforGFF/Covariance/Position.lean#L195), [`double_integral_timeReflection_covariance`](../../OSforGFF/Covariance/Position.lean#L144), [`covariance_timeReflection_invariant`](../../OSforGFF/Covariance/Position.lean#L395), [`freeCovarianceℂ_bilinear_agrees_on_reals`](../../OSforGFF/Covariance/RealForm.lean#L50)

---

### [`freeCovarianceFormR_reflection_cross`](../../OSforGFF/Covariance/RealForm.lean#L682) — Lemma

**Statement**: A mixed time-reflection identity: $C_{\mathbb{R}}(\Theta_{\mathbb{R}} f, g) = C_{\mathbb{R}}(\Theta_{\mathbb{R}} g, f)$.

**Proof uses**: [`freeCovarianceFormR_reflection_invariant`](../../OSforGFF/Covariance/RealForm.lean#L601), [`freeCovarianceFormR_symm`](../../OSforGFF/Covariance/RealForm.lean#L476)

---

### [`freeCovarianceFormR_left_linear_any_right`](../../OSforGFF/Covariance/RealForm.lean#L724) — Lemma

**Statement**: For finite linear combinations of positive-time test functions $f_i$ and arbitrary coefficients $c_i$, the covariance bilinear form is linear in the first argument over a finite sum: $\sum_{i\in s} c_i\,C_{\mathbb{R}}(\Theta_{\mathbb{R}} f_i, g) = C_{\mathbb{R}}\!\left(\sum_{i\in s} c_i\,\Theta_{\mathbb{R}} f_i,\; g\right)$.

**Proof uses**: [`freeCovarianceFormR_zero_left`](../../OSforGFF/Covariance/RealForm.lean#L588), [`freeCovarianceFormR_smul_left`](../../OSforGFF/Covariance/RealForm.lean#L512), [`freeCovarianceFormR_add_left`](../../OSforGFF/Covariance/RealForm.lean#L488)

---

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