# `TestFubini.lean` — Informal Summary

> **Source**: [`Bochner/TestFubini.lean`](../../Bochner/TestFubini.lean)
> **Generated**: 2026-03-10
> **Note**: Auto-generated by `/lean-summarize`. Re-run to refresh.

## Overview

Auxiliary Fubini lemmas for Gaussian regularization, including a Fubini identity for characteristic functions and second moment bounds on quadratic forms. This file provides the core Gaussian integration machinery used by both the Bochner and Minlos proof paths: the Fubini identity relating $\int_\mu (1 - e^{-\sigma^2 \lVert y \rVert^2/2})$ to a Gaussian-weighted integral of $1 - \mathrm{Re}(\varphi)$, and the bound $C^{-1} \int g_\sigma(x)\, \langle x, Sx \rangle\, dx \leq \sigma^2 T$ via spectral decomposition.

## Status

**Main result**: Fully proven (0 sorries, 0 axioms)
**Length**: 518 lines, 1 definition(s) + 19 theorem(s)/lemma(s)

---

## Gaussian Density

### [`gaussDensity`](../../Bochner/TestFubini.lean#L24) — Definition

**Lean signature**
```lean
private abbrev gaussDensity (σ : ℝ) (x : V) : ℝ :=
  Real.exp (-(1 / (2 * σ ^ 2)) * ‖x‖ ^ 2)
```

**Informal**: Unnormalized Gaussian density with scaling parameter $\sigma$: $g_\sigma(x) = \exp\!\bigl(-\lVert x \rVert^2 / (2\sigma^2)\bigr)$.

---

### [`gaussDensity_nonneg`](../../Bochner/TestFubini.lean#L27) — Lemma

**Statement**: $g_\sigma(x) \geq 0$.

**Proof uses**: `Real.exp_nonneg`

---

### [`gaussDensity_integrable`](../../Bochner/TestFubini.lean#L30) — Lemma

**Statement**: $g_\sigma$ is integrable for $\sigma > 0$.

**Proof uses**: `GaussianFourier.integrable_cexp_neg_mul_sq_norm_add`

---

### [`gaussDensity_integral_pos`](../../Bochner/TestFubini.lean#L44) — Lemma

**Statement**: $\int g_\sigma(x)\, dx > 0$ for $\sigma > 0$.

**Proof uses**: `integral_pos_of_integrable_nonneg_nonzero`, [`gaussDensity_integrable`](../../Bochner/TestFubini.lean#L30), [`gaussDensity_nonneg`](../../Bochner/TestFubini.lean#L27)

---

### [`gaussian_fourier_eq`](../../Bochner/TestFubini.lean#L53) — Lemma

**Statement**: The Gaussian integral with an exponential phase equals $C \cdot e^{-\sigma^2 \lVert y \rVert^2/2}$:
$$\int g_\sigma(x)\, e^{i\langle y, x \rangle}\, dx = C \cdot e^{-\sigma^2 \lVert y \rVert^2/2}$$
where $C = \int g_\sigma$.

**Proof uses**: `GaussianFourier.integral_cexp_neg_mul_sq_norm_add`, `GaussianFourier.integral_rexp_neg_mul_sq_norm`, `Complex.ofReal_cpow`

---

## Integrability helpers

### [`exp_neg_sq_integrable_prob`](../../Bochner/TestFubini.lean#L82) — Lemma

**Statement**: $y \mapsto e^{-\sigma^2 \lVert y \rVert^2/2}$ is integrable w.r.t. a probability measure.

**Proof uses**: `Real.exp_le_exp_of_le`, `integrable_const`

---

### [`cexp_neg_sq_integrable_prob`](../../Bochner/TestFubini.lean#L92) — Lemma

**Statement**: The complex version $y \mapsto \mathrm{cexp}(-\sigma^2 \lVert y \rVert^2/2)$ is integrable w.r.t. a probability measure.

**Proof uses**: [`exp_neg_sq_integrable_prob`](../../Bochner/TestFubini.lean#L82)

---

### [`gaussDensity_mul_charFun_re_integrable`](../../Bochner/TestFubini.lean#L100) — Lemma

**Statement**: $g_\sigma \cdot \mathrm{Re}(\varphi)$ is integrable, where $\varphi$ is the characteristic function of a probability measure.

**Proof uses**: [`gaussDensity_integrable`](../../Bochner/TestFubini.lean#L30), `norm_charFun_le_one`

---

### [`gaussDensity_mul_charFun_integrable`](../../Bochner/TestFubini.lean#L115) — Lemma

**Statement**: $g_\sigma \cdot \varphi$ is integrable (complex-valued).

**Proof uses**: [`gaussDensity_integrable`](../../Bochner/TestFubini.lean#L30), `norm_charFun_le_one`

---

## Fubini identity

### [`fubini_gaussian_charFun'`](../../Bochner/TestFubini.lean#L134) — Lemma

**Statement**: Fubini identity for Gaussian averaging:
$$\int_\mu \bigl(1 - e^{-\sigma^2 \lVert y \rVert^2/2}\bigr) = C^{-1} \int g_\sigma(x)\, \bigl(1 - \mathrm{Re}(\varphi(x))\bigr)\, dx.$$

**Proof uses**: `integral_integral_swap`, [`gaussian_fourier_eq`](../../Bochner/TestFubini.lean#L53), `Complex.reCLM.integral_comp_comm`, [`exp_neg_sq_integrable_prob`](../../Bochner/TestFubini.lean#L82), [`cexp_neg_sq_integrable_prob`](../../Bochner/TestFubini.lean#L92), [`gaussDensity_mul_charFun_re_integrable`](../../Bochner/TestFubini.lean#L100), [`gaussDensity_mul_charFun_integrable`](../../Bochner/TestFubini.lean#L115), [`gaussDensity_integral_pos`](../../Bochner/TestFubini.lean#L44)

---

## Gaussian second moment bound

### [`gaussian_real_formula`](../../Bochner/TestFubini.lean#L225) — Lemma

**Statement**: The real Gaussian integral formula as a function of parameter $c$:
$$\int e^{-b\lVert x \rVert^2 + c\langle w, x \rangle}\, dx = C \cdot e^{c^2 \lVert w \rVert^2 / (4b)}.$$

**Proof uses**: `GaussianFourier.integral_cexp_neg_mul_sq_norm_add`, `GaussianFourier.integral_cexp_neg_mul_sq_norm`

---

### [`id_le_sinh`](../../Bochner/TestFubini.lean#L250) — Lemma

**Statement**: $t \leq \sinh(t)$ for $t \geq 0$.

**Proof uses**: `monotoneOn_of_deriv_nonneg`, `Real.hasDerivAt_sinh`, `Real.one_le_cosh`

---

### [`half_sq_le_cosh_sub_one`](../../Bochner/TestFubini.lean#L266) — Lemma

**Statement**: $x^2/2 \leq \cosh(x) - 1$.

**Proof uses**: [`id_le_sinh`](../../Bochner/TestFubini.lean#L250), `Real.cosh_two_mul`, `Real.cosh_sq`

---

### [`gaussDensity_mul_exp_inner_integrable`](../../Bochner/TestFubini.lean#L293) — Lemma

**Statement**: $g_\sigma(x) \cdot e^{c\langle w, x \rangle}$ is integrable.

**Proof uses**: `GaussianFourier.integrable_cexp_neg_mul_sq_norm_add`

---

### [`gaussDensity_exp_inner_integral`](../../Bochner/TestFubini.lean#L312) — Lemma

**Statement**: $\int g_\sigma(x)\, e^{c\langle w, x \rangle}\, dx = C \cdot e^{c^2 \sigma^2 \lVert w \rVert^2/2}$.

**Proof uses**: [`gaussian_real_formula`](../../Bochner/TestFubini.lean#L225)

---

### [`tendsto_exp_slope`](../../Bochner/TestFubini.lean#L326) — Lemma

**Statement**: $(e^{tA} - 1)/t \to A$ as $t \to 0^+$.

**Proof uses**: `Real.hasDerivAt_exp`, `HasDerivAt.tendsto_slope_zero_right`

---

### [`gaussDensity_mul_cosh_integrable`](../../Bochner/TestFubini.lean#L341) — Lemma

**Statement**: $g_\sigma(x) \cdot \cosh(c\langle w, x \rangle)$ is integrable.

**Proof uses**: [`gaussDensity_mul_exp_inner_integrable`](../../Bochner/TestFubini.lean#L293), `Real.cosh_eq`

---

### [`gaussDensity_cosh_integral`](../../Bochner/TestFubini.lean#L359) — Lemma

**Statement**: $\int g_\sigma(x) \cosh(c\langle w, x \rangle)\, dx = C \cdot e^{c^2 \sigma^2 \lVert w \rVert^2/2}$.

**Proof uses**: [`gaussDensity_exp_inner_integral`](../../Bochner/TestFubini.lean#L312), [`gaussDensity_mul_exp_inner_integrable`](../../Bochner/TestFubini.lean#L293)

---

### [`gaussDensity_mul_inner_sq_integrable`](../../Bochner/TestFubini.lean#L380) — Lemma

**Statement**: $g_\sigma(x) \cdot \langle w, x \rangle^2$ is integrable.

**Proof uses**: [`gaussDensity_mul_cosh_integrable`](../../Bochner/TestFubini.lean#L341), [`half_sq_le_cosh_sub_one`](../../Bochner/TestFubini.lean#L266)

---

### [`gaussian_inner_sq_le`](../../Bochner/TestFubini.lean#L394) — Lemma

**Statement**: $\int g_\sigma(x)\, \langle w, x \rangle^2\, dx \leq C \cdot \sigma^2 \lVert w \rVert^2$.

**Proof uses**: [`gaussDensity_cosh_integral`](../../Bochner/TestFubini.lean#L359), [`half_sq_le_cosh_sub_one`](../../Bochner/TestFubini.lean#L266), [`tendsto_exp_slope`](../../Bochner/TestFubini.lean#L326), [`gaussDensity_mul_inner_sq_integrable`](../../Bochner/TestFubini.lean#L380), [`gaussDensity_mul_cosh_integrable`](../../Bochner/TestFubini.lean#L341), [`gaussDensity_integral_pos`](../../Bochner/TestFubini.lean#L44)

---

### [`gaussian_quadForm_integral_le'`](../../Bochner/TestFubini.lean#L444) — Lemma

**Statement**: Gaussian second moment bound for a positive operator $S$ with trace bound $T$:
$$C^{-1} \int g_\sigma(x)\, \langle x, Sx \rangle\, dx \leq \sigma^2\, T.$$

**Proof uses**: spectral decomposition (`LinearMap.IsSymmetric.eigenvectorBasis`, `LinearMap.IsSymmetric.eigenvalues`), [`gaussian_inner_sq_le`](../../Bochner/TestFubini.lean#L394), [`gaussDensity_integral_pos`](../../Bochner/TestFubini.lean#L44), [`gaussDensity_mul_inner_sq_integrable`](../../Bochner/TestFubini.lean#L380)

---

*This file has **1** definition and **19** theorems/lemmas (0 with sorry).*