# `Main.lean` — Informal Summary

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

## Overview

This file proves **Bochner's theorem**: a continuous positive-definite function $\varphi : V \to \mathbb{C}$ with $\varphi(0) = 1$ on a finite-dimensional real inner product space is the characteristic function of a unique probability measure on $V$. The proof proceeds through five phases: (1) showing that $L^1$ positive-definite functions have nonnegative real Fourier transforms via Fejer averaging, (2) Gaussian regularization to produce $L^1$ approximations, (3) constructing probability measures from $L^1$ PD functions via Fourier inversion, (4) establishing tightness and extracting a weak limit via Prokhorov's theorem, and (5) uniqueness from Mathlib's `Measure.ext_of_charFun`.

## Status

**Main result**: `bochner_theorem` -- fully proven.
**Gaps**: None -- file is sorry-free.
**Length**: 1297 lines, 1 definition(s) + 27 theorem(s)/lemma(s)

---

## Phase 1: $L^1$ positive-definite functions have nonneg Fourier transform

### [`sum_star_mul_eq_normSq`](../../Bochner/Main.lean#L90) — Lemma (private)

**Statement**: The double sum $\sum_i \sum_j \overline{a_i} \, a_j$ equals $\lvert\sum_k a_k\rvert^2$ (as a complex number cast from `normSq`).

**Proof uses**: `starRingEnd_apply`, `Complex.normSq_eq_conj_mul_self`, `Finset.sum_mul_sum`

---

## Phase 1.5: Characteristic functions are positive definite

### [`isPositiveDefinite_charFun`](../../Bochner/Main.lean#L111) — Lemma

**Statement**: The characteristic function of any finite measure $\mu$ is positive definite: $\sum_{i,j} \overline{c_i}\,c_j\,\hat\mu(t_i - t_j) = \int \lvert\sum_k c_k e^{i\langle x,t_k\rangle}\rvert^2\,d\mu(x) \ge 0$.

**Proof uses**: [`sum_star_mul_eq_normSq`](../../Bochner/Main.lean#L90), `charFun_apply`, `charFun_neg`, `integral_finset_sum`, `Complex.reCLM.integral_comp_comm`

---

### [`isPositiveDefinite_mul_charFun`](../../Bochner/Main.lean#L205) — Lemma

**Statement**: The pointwise product $t \mapsto \varphi(t)\,\hat\mu(t)$ of a positive-definite function $\varphi$ and the characteristic function of a finite measure $\mu$ is positive definite (a continuous Schur product).

**Proof uses**: [`IsPositiveDefinite`](../../Bochner/PositiveDefinite.lean#L63), `charFun_apply`, `charFun_neg`, `integral_finset_sum`, `Complex.reCLM.integral_comp_comm`

---

### [`gaussian_eq_charFun`](../../Bochner/Main.lean#L298) — Lemma (private)

**Statement**: For $\varepsilon > 0$, there exists a finite measure $\mu$ on $V$ whose characteristic function satisfies $\hat\mu(t) = e^{-\varepsilon \lVert t \rVert^2}$.

**Proof uses**: `Measure.withDensity`, `GaussianFourier.integrable_cexp_neg_mul_sq_norm_add`, `GaussianFourier.integral_cexp_neg_mul_sq_norm_add`, `integral_withDensity_eq_integral_toReal_smul₀`

---

### [`isPositiveDefinite_gaussian`](../../Bochner/Main.lean#L379) — Lemma

**Statement**: The Gaussian $x \mapsto e^{-\varepsilon\lVert x\rVert^2}$ is positive definite for $\varepsilon > 0$, since it is the characteristic function of a centered Gaussian measure.

**Proof uses**: [`gaussian_eq_charFun`](../../Bochner/Main.lean#L298), [`isPositiveDefinite_charFun`](../../Bochner/Main.lean#L111)

---

## Phase 2: Gaussian regularization

### [`gaussianRegularize`](../../Bochner/Main.lean#L391) — Definition

**Lean signature**
```lean
noncomputable def gaussianRegularize (φ : V → ℂ) (ε : ℝ) : V → ℂ
```
**Informal**: The Gaussian-regularized function $\varphi_\varepsilon(x) = \varphi(x)\cdot e^{-\varepsilon\lVert x\rVert^2}$.

---

### [`gaussianRegularize_pd`](../../Bochner/Main.lean#L405) — Lemma

**Statement**: $\varphi_\varepsilon$ is positive definite whenever $\varphi$ is positive definite and $\varepsilon > 0$.

**Proof uses**: [`gaussian_eq_charFun`](../../Bochner/Main.lean#L298), [`isPositiveDefinite_mul_charFun`](../../Bochner/Main.lean#L205)

---

### [`gaussianRegularize_integrable`](../../Bochner/Main.lean#L427) — Lemma

**Statement**: $\varphi_\varepsilon$ is integrable for $\varepsilon > 0$, since $\lVert\varphi(x)\rVert \le \mathrm{Re}(\varphi(0))$ (bounded) and the Gaussian factor provides exponential decay.

**Proof uses**: [`IsPositiveDefinite.bounded_by_zero`](../../Bochner/PositiveDefinite.lean#L130), [`IsPositiveDefinite.eval_zero_nonneg`](../../Bochner/PositiveDefinite.lean#L106), `GaussianFourier.integrable_cexp_neg_mul_sq_norm_add`

---

### [`gaussianRegularize_zero`](../../Bochner/Main.lean#L448) — Lemma

**Statement**: $\varphi_\varepsilon(0) = \varphi(0)$.

**Proof uses**: (direct computation)

---

### [`gaussianRegularize_tendsto`](../../Bochner/Main.lean#L454) — Lemma

**Statement**: $\varphi_\varepsilon(x) \to \varphi(x)$ pointwise as $\varepsilon \to 0^+$.

**Proof uses**: `Filter.Tendsto.cexp`, `tendsto_nhdsWithin_of_tendsto_nhds`

---

## Phase 1 proof: $\mathrm{Re}(\mathcal{F}\varphi(\xi)) \ge 0$ for $L^1$ PD functions

### [`pd_l1_fourier_re_nonneg_ax`](../../Bochner/Main.lean#L483) — Theorem

**Statement**: If $\varphi$ is positive definite, continuous, and integrable, then $\mathrm{Re}(\mathcal{F}\varphi(\xi)) \ge 0$ for all $\xi$. This is the axiomatic bridge to the Fejer-based proof in `FejerPD.lean`.

**Proof uses**: [`pd_l1_fourier_re_nonneg_theorem`](../../Bochner/FejerPD.lean#L576)

---

### [`gaussianRegularize_norm_le`](../../Bochner/Main.lean#L493) — Lemma (private)

**Statement**: $\lVert\varphi_\varepsilon(x)\rVert \le \lVert\varphi(x)\rVert$ for $\varepsilon \ge 0$.

**Proof uses**: `Complex.norm_exp`, `Real.exp_le_one_iff`

---

### [`ft_gaussianRegularize_tendsto`](../../Bochner/Main.lean#L505) — Lemma (private)

**Statement**: $\mathcal{F}(\varphi_\varepsilon)(\xi) \to \mathcal{F}(\varphi)(\xi)$ as $\varepsilon \to 0^+$, by dominated convergence with dominating function $\lVert\varphi\rVert$.

**Proof uses**: [`gaussianRegularize_norm_le`](../../Bochner/Main.lean#L493), [`gaussianRegularize_tendsto`](../../Bochner/Main.lean#L454), `tendsto_integral_filter_of_dominated_convergence`

---

### [`pd_l1_fourier_re_nonneg`](../../Bochner/Main.lean#L531) — Theorem

**Statement**: If $\varphi$ is positive definite, continuous, and integrable, then $\mathrm{Re}(\mathcal{F}\varphi(\xi)) \ge 0$ for all $\xi$.

**Proof uses**: [`pd_l1_fourier_re_nonneg_ax`](../../Bochner/Main.lean#L483)

---

### [`pd_l1_fourier_nonneg`](../../Bochner/Main.lean#L538) — Lemma

**Statement**: If $\varphi$ is $L^1$ and positive definite, then $\mathrm{Re}(\mathcal{F}\varphi(\xi)) \ge 0$ and $\mathrm{Im}(\mathcal{F}\varphi(\xi)) = 0$ for all $\xi$. The imaginary part vanishes by Hermitian symmetry $\varphi(-x) = \overline{\varphi(x)}$ and the substitution $v \mapsto -v$.

**Proof uses**: [`pd_l1_fourier_re_nonneg`](../../Bochner/Main.lean#L531), `integral_neg_eq_self`, `integral_conj`

---

### [`pd_l1_fourier_real_nonneg`](../../Bochner/Main.lean#L567) — Lemma

**Statement**: $\mathcal{F}\varphi(\xi) = \mathrm{Re}(\mathcal{F}\varphi(\xi))$ (real-valued) and $\mathrm{Re}(\mathcal{F}\varphi(\xi)) \ge 0$.

**Proof uses**: [`pd_l1_fourier_nonneg`](../../Bochner/Main.lean#L538)

---

## Phase 3: Construct probability measures from $L^1$ PD functions

### [`measure_of_pd_l1`](../../Bochner/Main.lean#L587) — Lemma

**Statement**: Given $\varphi \in L^1$ positive definite with $\varphi(0) = 1$ and $\mathcal{F}\varphi \in L^1$, there exists a probability measure $\mu$ with $\hat\mu = \varphi$. The measure is $d\mu = \mathcal{F}\psi \cdot d\lambda$ where $\psi(x) = \varphi(2\pi x)$ absorbs the Fourier convention difference, and total mass equals $\psi(0) = 1$ by Fourier inversion.

**Proof uses**: [`pd_l1_fourier_nonneg`](../../Bochner/Main.lean#L538), [`isPositiveDefinite_precomp_linear`](../../Bochner/PositiveDefinite.lean#L70), `Measure.withDensity`, `Integrable.fourierInv_fourier_eq`, `Continuous.fourierInv_fourier_eq`, `integral_withDensity_eq_integral_toReal_smul₀`

---

## Phase 4: Tightness and weak limit

### [`parseval_l1`](../../Bochner/Main.lean#L743) — Lemma (private)

**Statement**: $L^1$ Parseval/Fubini identity: $\int \mathcal{F}f(\xi)\,g(\xi)\,d\xi = \int f(x)\,\mathcal{F}g(x)\,dx$ for $f, g \in L^1$.

**Proof uses**: `VectorFourier.integral_fourierIntegral_smul_eq_flip`

---

### [`gaussian_cexp_integrable`](../../Bochner/Main.lean#L755) — Lemma (private)

**Statement**: The complex Gaussian $\xi \mapsto e^{-t\lVert\xi\rVert^2}$ is integrable for $t > 0$.

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

---

### [`ft_gaussian_integrable`](../../Bochner/Main.lean#L763) — Lemma (private)

**Statement**: The Fourier transform of the Gaussian $e^{-t\lVert\xi\rVert^2}$ is integrable (it is also a Gaussian).

**Proof uses**: [`gaussian_cexp_integrable`](../../Bochner/Main.lean#L755), `fourier_gaussian_innerProductSpace`

---

### [`integral_ft_gaussian_eq_one`](../../Bochner/Main.lean#L777) — Lemma (private)

**Statement**: $\int \mathcal{F}(e^{-t\lVert\cdot\rVert^2})(x)\,dx = 1$ for $t > 0$, by Fourier inversion at the origin.

**Proof uses**: [`gaussian_cexp_integrable`](../../Bochner/Main.lean#L755), [`ft_gaussian_integrable`](../../Bochner/Main.lean#L763), `Continuous.fourierInv_fourier_eq`

---

### [`integral_norm_ft_gaussian_eq_one`](../../Bochner/Main.lean#L791) — Lemma (private)

**Statement**: $\int \lVert\mathcal{F}(e^{-t\lVert\cdot\rVert^2})(x)\rVert\,dx = 1$ for $t > 0$, since the Fourier transform of a PD Gaussian is nonneg real.

**Proof uses**: [`isPositiveDefinite_gaussian`](../../Bochner/Main.lean#L379), [`pd_l1_fourier_nonneg`](../../Bochner/Main.lean#L538), [`integral_ft_gaussian_eq_one`](../../Bochner/Main.lean#L777)

---

### [`gaussianRegularize_ft_integrable`](../../Bochner/Main.lean#L821) — Theorem

**Statement**: The Fourier transform $\mathcal{F}(\varphi_\varepsilon)$ is integrable for $\varepsilon > 0$. Proved by bounding each approximant $\int \mathcal{F}(\varphi_\varepsilon)\cdot e^{-t\lVert\cdot\rVert^2} \le \mathrm{Re}(\varphi(0))$ via $L^1$ Parseval, then applying Fatou's lemma as $t \to 0$.

**Proof uses**: [`gaussianRegularize_pd`](../../Bochner/Main.lean#L405), [`gaussianRegularize_integrable`](../../Bochner/Main.lean#L427), [`pd_l1_fourier_nonneg`](../../Bochner/Main.lean#L538), [`parseval_l1`](../../Bochner/Main.lean#L743), [`integral_norm_ft_gaussian_eq_one`](../../Bochner/Main.lean#L791), `lintegral_liminf_le`

---

### [`one_sub_exp_neg_le`](../../Bochner/Main.lean#L973) — Lemma (private)

**Statement**: $1 - e^{-x} \le x$ for $x \ge 0$.

**Proof uses**: `Real.one_sub_le_exp_neg`

---

### [`gaussianRegularize_deviation_bound`](../../Bochner/Main.lean#L979) — Lemma (private)

**Statement**: $\lVert 1 - \varphi_\varepsilon(v)\rVert \le \lVert 1 - \varphi(v)\rVert + \lVert v\rVert^2$ for $\varphi$ PD with $\varphi(0)=1$ and $0 < \varepsilon \le 1$.

**Proof uses**: [`IsPositiveDefinite.bounded_by_zero`](../../Bochner/PositiveDefinite.lean#L130), [`one_sub_exp_neg_le`](../../Bochner/Main.lean#L973)

---

### [`charFun_measure_inner_bound`](../../Bochner/Main.lean#L1017) — Lemma (private)

**Statement**: If $\mu$ is a probability measure with $\hat\mu = \varphi_\varepsilon$ ($\varepsilon \le 1$), then $\mu^{\mathrm{real}}\{x \mid r < \lvert\langle y,x\rangle\rvert\} \le 2C + 8\lVert y\rVert^2 r^{-2}$, where $C$ bounds $\lVert 1 - \varphi(t\cdot y)\rVert$ for $\lvert t\rvert \le 2/r$.

**Proof uses**: [`gaussianRegularize_deviation_bound`](../../Bochner/Main.lean#L979), `measureReal_abs_inner_gt_le_integral_charFun`, `intervalIntegral.norm_integral_le_of_norm_le_const`

---

### [`gaussianRegularize_measures_tight`](../../Bochner/Main.lean#L1070) — Theorem

**Statement**: The family $\{\mu_\varepsilon : 0 < \varepsilon \le 1,\; \hat\mu_\varepsilon = \varphi_\varepsilon\}$ of probability measures is tight, using the inner-product criterion for tightness and continuity of $\varphi$ at $0$.

**Proof uses**: [`charFun_measure_inner_bound`](../../Bochner/Main.lean#L1017), `isTightMeasureSet_of_inner_tendsto`

---

## Phase 5: Uniqueness (from Mathlib)

## Main Theorem

### [`bochner_theorem`](../../Bochner/Main.lean#L1190) — Theorem

**Statement**: If $\varphi : V \to \mathbb{C}$ is continuous, positive definite, and $\varphi(0) = 1$ on a finite-dimensional real inner product space $V$, then there exists a unique probability measure $\mu$ on $V$ such that $\hat\mu = \varphi$.

**Proof uses**: [`measure_of_pd_l1`](../../Bochner/Main.lean#L587), [`gaussianRegularize_pd`](../../Bochner/Main.lean#L405), [`gaussianRegularize_integrable`](../../Bochner/Main.lean#L427), [`gaussianRegularize_zero`](../../Bochner/Main.lean#L448), [`gaussianRegularize_ft_integrable`](../../Bochner/Main.lean#L821), [`gaussianRegularize_measures_tight`](../../Bochner/Main.lean#L1070), [`gaussianRegularize_tendsto`](../../Bochner/Main.lean#L454), `isCompact_closure_of_isTightMeasureSet`, `ProbabilityMeasure.tendsto_iff_forall_integral_rclike_tendsto`, `Measure.ext_of_charFun`

---

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