# `FinDimMarginals.lean` — Informal Summary

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

## Overview

Given a continuous positive-definite normalized functional $\Phi$ on a topological vector space $E$, this file constructs finite-dimensional marginal measures via Bochner's theorem. For test vectors $f_1, \ldots, f_n \in E$, the marginal characteristic function $\Phi_F(t) = \Phi\bigl(\sum_i t_i \cdot f_i\bigr)$ is a continuous positive-definite function on $\mathbb{R}^n$ with $\Phi_F(0) = 1$, so the (finite-dimensional) Bochner theorem yields a unique probability measure $\mu_F$ on $\mathbb{R}^n$ whose characteristic function equals $\Phi_F$. This is the core step that reduces the infinite-dimensional Minlos problem to the finite-dimensional Bochner result.

## Status

**Main result**: [`marginal_measure_exists`](../../Minlos/FinDimMarginals.lean#L84) -- Bochner's theorem applied to finite-dimensional marginals.
**Length**: 96 lines, 2 definition(s) + 4 theorem(s)/lemma(s)

---

### `marginalCF` (definition, L36)

[`marginalCF`](../../Minlos/FinDimMarginals.lean#L36)

```lean
def marginalCF {E : Type*} [AddCommGroup E] [Module ℝ E]
    (Φ : E → ℂ) {n : ℕ} (f : Fin n → E) :
    EuclideanSpace ℝ (Fin n) → ℂ
```

The finite-dimensional marginal characteristic function. Given a functional $\Phi : E \to \mathbb{C}$ and test vectors $f : \mathrm{Fin}\; n \to E$, defines $\Phi_F(t) = \Phi\bigl(\sum_i t_i \cdot f_i\bigr)$ on $\mathrm{EuclideanSpace}\;\mathbb{R}\;(\mathrm{Fin}\; n)$.

---

### `marginalCF_continuous` (theorem, L46)

[`marginalCF_continuous`](../../Minlos/FinDimMarginals.lean#L46)

If $\Phi : E \to \mathbb{C}$ is continuous and $E$ is a topological $\mathbb{R}$-module, then $\mathrm{marginalCF}\;\Phi\;f$ is continuous.

**Proof sketch**: Each summand $t_i \cdot f_i$ is continuous in $t$ (continuous coordinate projection composed with continuous scalar multiplication). A finite sum of continuous functions is continuous. Composing with the continuous $\Phi$ gives the result.

**Dependencies**: `EuclideanSpace.proj`, `Continuous.comp`, `continuous_finset_sum`.

---

### `spanLinearMap` (private definition, L56)

[`spanLinearMap`](../../Minlos/FinDimMarginals.lean#L56)

```lean
private def spanLinearMap {E : Type*} [AddCommGroup E] [Module ℝ E]
    {n : ℕ} (f : Fin n → E) : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] E
```

The linear map $t \mapsto \sum_i t_i \cdot f_i$ from $\mathrm{EuclideanSpace}\;\mathbb{R}\;(\mathrm{Fin}\; n)$ to $E$. Used as an auxiliary in the proof that `marginalCF` preserves positive definiteness.

---

### `marginalCF_pd` (theorem, L68)

[`marginalCF_pd`](../../Minlos/FinDimMarginals.lean#L68)

If $\Phi : E \to \mathbb{C}$ is positive definite, then $\mathrm{marginalCF}\;\Phi\;f$ is positive definite on $\mathrm{EuclideanSpace}\;\mathbb{R}\;(\mathrm{Fin}\; n)$.

**Proof sketch**: Direct application of [`isPositiveDefinite_precomp_linear`](../../Bochner/PositiveDefinite.lean#L70): composing a positive-definite function with a linear map preserves positive definiteness.

**Dependencies**: [`isPositiveDefinite_precomp_linear`](../../Bochner/PositiveDefinite.lean#L70), [`spanLinearMap`](../../Minlos/FinDimMarginals.lean#L56).

---

### `marginalCF_normalized` (theorem, L74)

[`marginalCF_normalized`](../../Minlos/FinDimMarginals.lean#L74)

If $\Phi(0) = 1$, then $\mathrm{marginalCF}\;\Phi\;f\;(0) = 1$.

**Proof sketch**: At $t = 0$, every summand $0 \cdot f_i = 0$, so the sum is $0$ and $\Phi_F(0) = \Phi(0) = 1$.

**Dependencies**: None beyond the definition of [`marginalCF`](../../Minlos/FinDimMarginals.lean#L36).

---

### `marginal_measure_exists` (theorem, L84)

[`marginal_measure_exists`](../../Minlos/FinDimMarginals.lean#L84)

For each finite set of test vectors $f_1, \ldots, f_n \in E$, if $\Phi$ is continuous, positive definite, and normalized ($\Phi(0) = 1$), there exists a **unique** probability measure $\mu$ on $\mathrm{EuclideanSpace}\;\mathbb{R}\;(\mathrm{Fin}\; n)$ such that
$$\mathrm{charFun}(\mu)(\xi) = \mathrm{marginalCF}\;\Phi\;f\;(\xi) \quad \text{for all } \xi.$$

**Proof sketch**: Combine the three preceding results (`marginalCF_continuous`, `marginalCF_pd`, `marginalCF_normalized`) and apply [`bochner_theorem`](../../Bochner/Main.lean#L1190).

**Dependencies**: [`bochner_theorem`](../../Bochner/Main.lean#L1190), [`marginalCF_continuous`](../../Minlos/FinDimMarginals.lean#L46), [`marginalCF_pd`](../../Minlos/FinDimMarginals.lean#L68), [`marginalCF_normalized`](../../Minlos/FinDimMarginals.lean#L74).

---

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