# `Main.lean` — Informal Summary

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

## Overview

This file states and proves **Minlos' theorem**: on a nuclear, separable, locally convex space $E$, every continuous positive-definite normalized functional $\Phi : E \to \mathbb{C}$ is the characteristic functional of a unique probability measure $\mu$ on the topological dual $E' = \mathrm{WeakDual}_{\mathbb{R}}\, E$. The proof assembles finite-dimensional Bochner marginals, the Kolmogorov projective extension, a measurable projection from $E \to \mathbb{R}$ to $E'$, and a uniqueness argument. A corollary (`minlos_uniqueness`) extracts the uniqueness statement separately.

## Status

**Main result**: `minlos_theorem` -- fully proved (no sorry, no custom axioms)
**Length**: 212 lines, 0 definition(s) + 3 theorem(s)/lemma(s)

---

### [`trans_symm_apply_eq'`](../../Minlos/Main.lean#L38) — Private Lemma

**Statement**: For measurable equivalences $e_1 : \alpha \simeq_m \beta$ and $e_2 : \beta \simeq_m \gamma$, the inverse of their composition satisfies $(e_1 \circ e_2)^{-1}(z) = e_1^{-1}(e_2^{-1}(z))$.

**Proof**: Definitional (`rfl`).

---

### [`minlos_theorem`](../../Minlos/Main.lean#L58) — Theorem

**Statement**: Let $E$ be a type with `[AddCommGroup E]`, `[Module\;\mathbb{R}\;E]`, `[TopologicalSpace E]`, `[IsTopologicalAddGroup E]`, `[ContinuousSMul\;\mathbb{R}\;E]`, `[IsHilbertNuclear E]`, `[SeparableSpace E]`, `[Nonempty E]`. If $\Phi : E \to \mathbb{C}$ is continuous, positive-definite, and satisfies $\Phi(0) = 1$, then there exists a unique probability measure $\mu$ on $\mathrm{WeakDual}_{\mathbb{R}}\, E$ such that
$$\Phi(f) = \int_{E'} e^{i\,\omega(f)}\, d\mu(\omega) \quad \text{for all } f \in E.$$

**Proof outline** (5 steps):

1. Build the Kolmogorov projective limit $\nu$ on $E \to \mathbb{R}$ from the finite-dimensional marginals.
2. Prove that $\nu$ has the correct characteristic functional: for singletons ($h\_cf\_eq$) and for joint $n$-point marginals ($h\_cf\_joint$), the integrals $\int e^{i \sum s_k \omega(x_k)}\,d\nu = \Phi(\sum s_k x_k)$.
3. Push forward $\nu$ through the measurable projection $P$ to obtain $\mu = \nu.\mathrm{map}\, P$ on $\mathrm{WeakDual}_{\mathbb{R}}\, E$.
4. Verify that $\mu$ has CF equal to $\Phi$ (existence).
5. Prove uniqueness via the identity $P \circ \mathrm{embed} = \mathrm{id}$.

**Proof uses**:
- [`marginalProjectiveLimit`](../../Minlos/ProjectiveFamily.lean#L240) -- Kolmogorov extension yielding $\nu$ on $E \to \mathbb{R}$
- [`marginalProjectiveLimit_isProbability`](../../Minlos/ProjectiveFamily.lean#L247) -- $\nu$ is a probability measure
- [`marginalProjectiveLimit_isProjectiveLimit`](../../Minlos/ProjectiveFamily.lean#L255) -- projective limit property of $\nu$
- [`marginalFamily`](../../Minlos/ProjectiveFamily.lean#L67) -- the family of marginal measures indexed by finite subsets
- [`finsetPiMeasEquiv`](../../Minlos/ProjectiveFamily.lean#L42) -- measurable equivalence between $\prod_{j \in J} \mathbb{R}$ and $\mathrm{EuclideanSpace}\;\mathbb{R}\;(\mathrm{Fin}\;\lvert J\rvert)$
- [`finsetTestVectors`](../../Minlos/ProjectiveFamily.lean#L49) -- canonical test vectors for a finite subset $J \subseteq E$
- [`marginalMeasure_charFun`](../../Minlos/ProjectiveFamily.lean#L58) -- marginal CF equals $\Phi$ on test vector combinations
- [`marginalCF`](../../Minlos/FinDimMarginals.lean#L36) -- characteristic function of a marginal measure
- [`measurableProjection`](../../Minlos/MeasurableModification.lean#L580) -- measurable map $P : (E \to \mathbb{R}) \to \mathrm{WeakDual}_{\mathbb{R}}\, E$
- [`isProbabilityMeasure_map_projection`](../../Minlos/MeasurableModification.lean#L1013) -- $\nu.\mathrm{map}\, P$ is a probability measure
- [`charFunctional_map_projection`](../../Minlos/MeasurableModification.lean#L1019) -- CF of $\nu.\mathrm{map}\, P$ equals $\Phi$
- [`uniqueness_via_projection`](../../Minlos/MeasurableModification.lean#L1046) -- uniqueness via $P \circ \mathrm{embed} = \mathrm{id}$
- `Finset.measurable_restrict`, `integral_map`, `charFun_apply` -- Mathlib

---

### [`minlos_uniqueness`](../../Minlos/Main.lean#L199) — Theorem

**Statement**: Under the same hypotheses as `minlos_theorem`, if $\mu_1$ and $\mu_2$ are probability measures on $\mathrm{WeakDual}_{\mathbb{R}}\, E$ both satisfying
$$\int_{E'} e^{i\,\omega(f)}\, d\mu_k(\omega) = \Phi(f) \quad \text{for all } f \in E, \; k \in \{1, 2\},$$
then $\mu_1 = \mu_2$.

**Proof uses**:
- [`minlos_theorem`](../../Minlos/Main.lean#L58) -- extract the unique measure $\mu_0$ and apply uniqueness to both $\mu_1$ and $\mu_2$

---

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