# `MinlosConcentration.lean` — Informal Summary

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

## Overview

This file proves the **nuclear cylindrical concentration bound** (Gel'fand-Vilenkin Vol. 4, Ch. IV, S3.3): given a nuclear locally convex space $E$ equipped with Hilbertian seminorms $\{p_n\}$ with consecutive Hilbert-Schmidt embeddings generating the topology, a cylindrical probability measure $\nu$ with continuous normalized characteristic functional $\Phi$, and any dense sequence, for every $\varepsilon > 0$ there exist indices $m, C$ such that $\nu\{\omega \mid \exists c : \mathbb{N} \to_0 \mathbb{Q},\; \lvert\omega(x_c)\rvert > C \cdot p_m(x_c)\} < \varepsilon$. The proof combines CF-continuity-derived quadratic bounds, Gram-Schmidt orthonormalization for Hilbertian seminorms, dimension-free Gaussian averaging with Gram matrix trace bounds, Cauchy-Schwarz + Parseval concentration on good sets, Chebyshev tail estimates, and continuity of measure from below.

## Status

**Main result**: `nuclear_cylindrical_concentration` — fully proven (0 sorries, 0 axioms).

**Length**: 1832 lines, 2 definition(s) + 33 theorem(s)/lemma(s)

---

## CF constantly 1 implies zero a.e.

### [`ae_eq_zero_of_charfun_eq_one`](../../Minlos/MinlosConcentration.lean#L52) — Lemma

**Statement**: If a measurable random variable $X : \Omega \to \mathbb{R}$ has characteristic function constantly 1, i.e. $\int e^{i t X(\omega)}\,d\nu = 1$ for all $t \in \mathbb{R}$, then $X = 0$ $\nu$-a.e.

**Proof uses**: `Measure.ext_of_charFun`, `charFun_dirac`, `charFun_apply`, `integral_map`, `ae_dirac_iff`, `ae_map_iff`

---

## Helper lemmas

### [`cf_norm_le_one`](../../Minlos/MinlosConcentration.lean#L86) — Lemma

**Statement**: The characteristic functional satisfies $\lVert \Phi(x) \rVert \leq 1$, as the integral of a unit-modulus function against a probability measure.

**Proof uses**: `norm_integral_le_integral_norm`, `Complex.norm_exp`

---

### [`one_sub_re_le_two_of_norm_le`](../../Minlos/MinlosConcentration.lean#L104) — Lemma

**Statement**: If $\lVert z \rVert \leq 1$ then $1 - \mathrm{Re}(z) \leq 2$.

**Proof uses**: `abs_re_le_norm`

---

### [`quadratic_bound_outside`](../../Minlos/MinlosConcentration.lean#L112) — Lemma

**Statement**: Outside the ball $\{q(x) < \delta\}$, the real part deficit decays quadratically: if $\delta \leq q(x)$ and $\lVert \Phi(x) \rVert \leq 1$, then $1 - \mathrm{Re}(\Phi(x)) \leq (2/\delta^2) \cdot q(x)^2$.

**Proof uses**: [`one_sub_re_le_two_of_norm_le`](../../Minlos/MinlosConcentration.lean#L104)

---

### [`one_sub_re_nonneg`](../../Minlos/MinlosConcentration.lean#L127) — Lemma

**Statement**: Since $\lVert \Phi(x) \rVert \leq 1$, we have $1 - \mathrm{Re}(\Phi(x)) \geq 0$.

**Proof uses**: `abs_re_le_norm`

---

### [`cf_nhds_ball`](../../Minlos/MinlosConcentration.lean#L138) — Lemma

**Statement**: From $\Phi$ continuous with $\Phi(0) = 1$ and `WithSeminorms p`, there exist a finite set of seminorm indices $s$ and radius $r > 0$ such that $(\sup_{n \in s} p_n)(x) < r$ implies $\lVert 1 - \Phi(x) \rVert < \varepsilon$.

**Proof uses**: `WithSeminorms.hasBasis_zero_ball`, `Seminorm.ball_zero_eq`

---

## Monotonicity from consecutive HS embeddings

### [`seminorm_mono_of_le`](../../Minlos/MinlosConcentration.lean#L162) — Lemma

**Statement**: Consecutive Hilbert-Schmidt embeddings imply monotonicity: $p_n \leq p_m$ when $n \leq m$.

**Proof uses**: `IsHilbertSchmidtEmbedding` (first component), induction on $m$

---

### [`finset_sup_le_of_mono`](../../Minlos/MinlosConcentration.lean#L175) — Lemma

**Statement**: If seminorms are monotone and $m$ dominates all indices in $s$, then $\sup_{n \in s} p_n \leq p_m$.

**Proof uses**: [`seminorm_mono_of_le`](../../Minlos/MinlosConcentration.lean#L162), `Finset.sup_le`

---

## Combined quadratic bound

### [`combined_quadratic_bound`](../../Minlos/MinlosConcentration.lean#L189) — Lemma

**Statement**: For any $\varepsilon > 0$, there exist $m_0 \in \mathbb{N}$ and $K \geq 0$ such that $1 - \mathrm{Re}(\Phi(x)) \leq \varepsilon + K \cdot p_{m_0}(x)^2$ for all $x$. Inside the seminorm ball the CF continuity gives $\lVert 1 - \Phi \rVert < \varepsilon$; outside the ball the quadratic bound dominates.

**Proof uses**: [`cf_nhds_ball`](../../Minlos/MinlosConcentration.lean#L138), [`cf_norm_le_one`](../../Minlos/MinlosConcentration.lean#L86), [`finset_sup_le_of_mono`](../../Minlos/MinlosConcentration.lean#L175), [`quadratic_bound_outside`](../../Minlos/MinlosConcentration.lean#L112)

---

## CF vanishes on seminorm kernel

### [`cf_kernel_of_ball_bound`](../../Minlos/MinlosConcentration.lean#L229) — Lemma

**Statement**: If $q(z) = 0$ and $\Phi$ is dominated by $q$ near zero (for any $\varepsilon > 0$, there exists a $q$-ball where $\lVert 1 - \Phi \rVert < \varepsilon$), then $\Phi(t \cdot z) = 1$ for all $t \in \mathbb{R}$. Proof: $q(t \cdot z) = \lvert t \rvert \cdot q(z) = 0 < r$ for any $r > 0$.

**Proof uses**: `map_smul_eq_mul`

---

## Linear combination a.e. from joint CF

### [`linear_combination_ae`](../../Minlos/MinlosConcentration.lean#L253) — Lemma

**Statement**: The joint CF condition forces $\omega(\sum_j \beta_j e_j) = \sum_j \beta_j \omega(e_j)$ for $\nu$-a.e. $\omega$, even for real (not just rational) coefficients and without assuming linearity of $\omega$.

**Proof uses**: [`ae_eq_zero_of_charfun_eq_one`](../../Minlos/MinlosConcentration.lean#L52), `h_cf_joint`

---

## Pushforward CF for finite evaluation maps

### [`pushforward_charfun_eq`](../../Minlos/MinlosConcentration.lean#L302) — Lemma

**Statement**: The pushforward of $\nu$ to $\mathbb{R}^k$ via evaluation at vectors $(e_0, \ldots, e_{k-1})$ has characteristic function $v \mapsto \Phi(\sum_j v_j e_j)$.

**Proof uses**: `integral_map`, `h_cf_joint`

---

## Concentration on good set via Cauchy-Schwarz + Parseval

### [`bound_on_good_set`](../../Minlos/MinlosConcentration.lean#L325) — Lemma

**Statement**: If $\omega$ is linear on combinations of a $p$-orthonormal sequence $\{e_j\}$ and $\sum_j \omega(e_j)^2 \leq R^2$, then for any linear combination $x = \sum_j \beta_j e_j$, we have $\lvert \omega(x) \rvert \leq R \cdot p(x)$.

**Proof uses**: `Seminorm.sq_sum_orthonormal`, `Finset.sum_mul_sq_le_sq_mul_sq`, `abs_le_of_sq_le_sq`

---

## Kernel elements vanish a.e.

### [`kernel_eval_ae_zero`](../../Minlos/MinlosConcentration.lean#L356) — Lemma

**Statement**: If $p(z) = 0$ and $\Phi(t \cdot z) = 1$ for all $t$, then $\omega(z) = 0$ for $\nu$-a.e. $\omega$.

**Proof uses**: [`ae_eq_zero_of_charfun_eq_one`](../../Minlos/MinlosConcentration.lean#L52), `h_cf_joint`

---

## Q-linearity for all Finsupp simultaneously

### [`q_linear_ae_all`](../../Minlos/MinlosConcentration.lean#L380) — Lemma

**Statement**: For $\nu$-a.e. $\omega$, linearity holds simultaneously for all $\mathbb{Q}$-linear combinations $c : \mathbb{N} \to_0 \mathbb{Q}$ of a given sequence. Uses countable intersection since $\mathbb{N} \to_0 \mathbb{Q}$ is countable.

**Proof uses**: [`linear_combination_ae`](../../Minlos/MinlosConcentration.lean#L253), `eventually_countable_forall`

---

## Bad set definitions for continuity from below

### [`concentrationBadSet`](../../Minlos/MinlosConcentration.lean#L412) — Definition

**Lean signature**
```lean
def concentrationBadSet (d : ℕ → E) (p : Seminorm ℝ E) (C : ℝ) :
    Set (E → ℝ)
```

**Informal**: The "bad set" $\{\omega \mid \exists\, c : \mathbb{N} \to_0 \mathbb{Q},\; \lvert \omega(x_c) \rvert > C \cdot p(x_c)\}$ where $x_c = \sum_i c_i d_i$.

---

### [`concentrationBadSetN`](../../Minlos/MinlosConcentration.lean#L421) — Definition

**Lean signature**
```lean
def concentrationBadSetN (d : ℕ → E) (p : Seminorm ℝ E) (C : ℝ) (N : ℕ) :
    Set (E → ℝ)
```

**Informal**: The restricted bad set $B_N$: same as `concentrationBadSet` but restricted to $\mathbb{Q}$-linear combinations with support in $\{0, \ldots, N-1\}$.

---

### [`concentrationBadSetN_mono`](../../Minlos/MinlosConcentration.lean#L429) — Lemma

**Statement**: $B_N \subseteq B_M$ when $N \leq M$ (monotonicity in support size).

**Proof uses**: `Finset.range_mono`

---

### [`concentrationBadSet_eq_iUnion`](../../Minlos/MinlosConcentration.lean#L439) — Lemma

**Statement**: The full bad set equals the union of the restricted bad sets: $B = \bigcup_N B_N$, since every finitely supported function has support contained in some $\{0, \ldots, N-1\}$.

**Proof uses**: `Finset.le_sup`

---

### [`concentrationBadSet_measure_le`](../../Minlos/MinlosConcentration.lean#L456) — Lemma

**Statement**: If $\nu(B_N) \leq \delta$ for all $N$, then $\nu(B) \leq \delta$, via continuity of measure from below.

**Proof uses**: [`concentrationBadSet_eq_iUnion`](../../Minlos/MinlosConcentration.lean#L439), [`concentrationBadSetN_mono`](../../Minlos/MinlosConcentration.lean#L429), `tendsto_measure_iUnion_atTop`

---

## Seminorm Gram-Schmidt

### [`gs_seminorm_add_kernel`](../../Minlos/MinlosConcentration.lean#L474) — Private Lemma

**Statement**: If $p(z) = 0$, then $p(x + z) = p(x)$.

**Proof uses**: `map_add_le_add`, `map_neg_eq_map`

---

### [`gs_seminorm_sub_kernel`](../../Minlos/MinlosConcentration.lean#L484) — Private Lemma

**Statement**: If $p(z) = 0$, then $p(x - z) = p(x)$.

**Proof uses**: [`gs_seminorm_add_kernel`](../../Minlos/MinlosConcentration.lean#L474)

---

### [`gs_innerProd_sub_left`](../../Minlos/MinlosConcentration.lean#L490) — Private Lemma

**Statement**: $\langle x_1 - x_2, y \rangle_p = \langle x_1, y \rangle_p - \langle x_2, y \rangle_p$ for the seminorm inner product.

**Proof uses**: `Seminorm.innerProd_add_left`, `Seminorm.innerProd_neg_left`

---

### [`gs_innerProd_smul_right`](../../Minlos/MinlosConcentration.lean#L497) — Private Lemma

**Statement**: $\langle x, a \cdot y \rangle_p = a \cdot \langle x, y \rangle_p$.

**Proof uses**: `Seminorm.innerProd_smul_left`, `Seminorm.innerProd_comm`

---

### [`gs_innerProd_sum_right`](../../Minlos/MinlosConcentration.lean#L503) — Private Lemma

**Statement**: $\langle x, \sum_{j \in s} f(j) \rangle_p = \sum_{j \in s} \langle x, f(j) \rangle_p$.

**Proof uses**: `Seminorm.innerProd_sum_left`, `Seminorm.innerProd_comm`

---

### [`gs_pythagoras`](../../Minlos/MinlosConcentration.lean#L511) — Private Lemma

**Statement**: Pythagorean theorem for Hilbertian seminorms: if $\langle x, y \rangle_p = 0$ then $p(x + y)^2 = p(x)^2 + p(y)^2$.

**Proof uses**: `Seminorm.IsHilbertian` (parallelogram identity)

---

### [`gram_schmidt_seminorm_aux`](../../Minlos/MinlosConcentration.lean#L523) — Lemma

**Statement**: For a Hilbertian seminorm $p$ and $N$ vectors $d_0, \ldots, d_{N-1}$, there exist $k$ vectors $e_0, \ldots, e_{k-1}$ that are $p$-orthonormal, and every linear combination $\sum_i \beta_i d_i$ decomposes as $(\sum_j \alpha_j e_j) + z$ where $p(z) = 0$ and $p(\sum_i \beta_i d_i)^2 = \sum_j \alpha_j^2$ (Parseval). Proved by induction on $N$ with case split on whether the residual $u = d_N - \mathrm{proj}$ lies in $\ker(p)$.

**Proof uses**: [`gs_seminorm_add_kernel`](../../Minlos/MinlosConcentration.lean#L474), [`gs_pythagoras`](../../Minlos/MinlosConcentration.lean#L511), `Seminorm.sq_sum_orthonormal`, `Seminorm.innerProd_self`, `Seminorm.innerProd_smul_left`, `Seminorm.innerProd_comm`

---

### [`gram_schmidt_seminorm`](../../Minlos/MinlosConcentration.lean#L690) — Lemma

**Statement**: Same as `gram_schmidt_seminorm_aux` but stated for the original type variable $E$ (thin wrapper).

**Proof uses**: [`gram_schmidt_seminorm_aux`](../../Minlos/MinlosConcentration.lean#L523)

---

## Per-N concentration bound

### [`concentrationBadSetN_measure_bound`](../../Minlos/MinlosConcentration.lean#L709) — Lemma

**Statement**: For each $N$, the restricted bad set $B_N$ has measure bounded by the tail probability: $\nu(B_N) \leq \nu\{\sum_j \omega(e_j)^2 > R^2\}$, where $\{e_j\}$ is a $p$-ONB with the Gram-Schmidt decomposition property and the CF vanishes on the $p$-kernel. On the a.e. set where all decompositions hold, Cauchy-Schwarz + Parseval gives $\lvert\omega(x_c)\rvert \leq R \cdot p(x_c)$.

**Proof uses**: [`kernel_eval_ae_zero`](../../Minlos/MinlosConcentration.lean#L356), [`linear_combination_ae`](../../Minlos/MinlosConcentration.lean#L253), `eventually_countable_forall`, `Finset.sum_mul_sq_le_sq_mul_sq`, `abs_le_of_sq_le_sq`

---

## Nuclear cylindrical concentration

### [`joint_kernel_bound_finite`](../../Minlos/MinlosConcentration.lean#L816) — Private Lemma

**Statement**: If $z_1, \ldots, z_n$ are kernel elements ($p_m(z_i) = 0$) and the quadratic CF bound gives $1 - \mathrm{Re}(\Phi(\sum t_i z_i)) \leq \varepsilon_q$ for all $t$, then $\nu\{\exists i,\; \omega(z_i) \neq 0\} \leq \mathrm{ofReal}(\varepsilon_q)$. Proved by pushforward to Euclidean space, Gaussian averaging via `fubini_gaussian_charFun`, exponential Chebyshev, and continuity from below.

**Proof uses**: `charFun_apply`, `fubini_gaussian_charFun`, `gaussDensity_integral_pos'`, `gaussDensity_mul_charFun_re_integrable'`, `gaussDensity_integrable'`, `gaussDensity_nonneg'`, `EuclideanSpace.norm_eq`, `integral_map`, `tendsto_measure_iUnion_atTop`

---

### [`kernel_concentration_bound`](../../Minlos/MinlosConcentration.lean#L1015) — Private Lemma

**Statement**: For a finite-dimensional restriction (support in $\{0, \ldots, N-1\}$), the probability that any $\mathbb{Q}$-linear combination disagrees with its ONB decomposition is at most $\mathrm{ofReal}(\varepsilon_q)$: $\nu\{\exists c,\; \omega(x_c) \neq \sum_j \alpha_j \omega(e_j)\} \leq \mathrm{ofReal}(\varepsilon_q)$. Combines linearity a.e. with [`joint_kernel_bound_finite`](../../Minlos/MinlosConcentration.lean#L816) via countable enumeration.

**Proof uses**: [`linear_combination_ae`](../../Minlos/MinlosConcentration.lean#L253), [`joint_kernel_bound_finite`](../../Minlos/MinlosConcentration.lean#L816), `eventually_countable_forall`, `exists_surjective_nat`, `tendsto_measure_iUnion_atTop`

---

### [`tail_bound_uniform`](../../Minlos/MinlosConcentration.lean#L1232) — Private Lemma

**Statement**: The tail probability $\nu\{\sum_j \omega(e_j)^2 > R^2\}$ can be made $\leq \delta$ by choosing $R$ large, **uniformly** over all dimensions $k$ and all $p_{\mathrm{outer}}$-orthonormal bases $\{e_j\}_{j < k}$. The bound depends only on $\varepsilon_q$, $K$, $C_{\mathrm{HS}}$, $\delta$ (not on $k$ or $e$). Constructs the Gram matrix $S$ with $\langle v, Sv \rangle = p_{\mathrm{inner}}(\sum v_j e_j)^2$, proves $S$ positive with $\mathrm{Tr}(S) \leq C_{\mathrm{HS}}$ via Parseval on any ONB of $V$, then applies Gaussian averaging with the quadratic form integral bound.

**Proof uses**: `fubini_gaussian_charFun`, `gaussDensity_integral_pos'`, `gaussDensity_mul_charFun_re_integrable'`, `gaussDensity_mul_quadForm_integrable'`, `gaussian_quadForm_integral_le`, `Seminorm.innerProd_self`, `Seminorm.innerProd_sum_left`, `EuclideanSpace.norm_eq`, `integral_map`, `OrthonormalBasis.sum_inner_mul_inner`, `EuclideanSpace.inner_single_left`, `EuclideanSpace.inner_single_right`

---

### [`badSetN_bound_with_kernel`](../../Minlos/MinlosConcentration.lean#L1608) — Private Lemma

**Statement**: For each $N$, $\nu(B_N) \leq \nu\{\sum_j \omega(e_j)^2 > R^2\} + \varepsilon_{\mathrm{ker}}$, where $\varepsilon_{\mathrm{ker}}$ bounds the kernel concentration probability. This version does not assume the CF kernel condition, instead accounting for the kernel contribution additively.

**Proof uses**: `Finset.sum_mul_sq_le_sq_mul_sq`, `abs_le_of_sq_le_sq`, `measure_union_le`

---

### [`nuclear_cylindrical_concentration`](../../Minlos/MinlosConcentration.lean#L1672) — Theorem

**Statement**: Given a separable nonempty locally convex space $E$ with topology generated by Hilbertian seminorms $\{p_n\}$ with consecutive Hilbert-Schmidt embeddings, and a cylindrical probability measure $\nu$ with continuous CF $\Phi$ ($\Phi(0) = 1$, joint CF property), for any dense sequence $d : \mathbb{N} \to E$ and any $\varepsilon > 0$, there exist $m, C \in \mathbb{N}$ such that
$$\nu\Bigl\{\omega \mid \exists\, c : \mathbb{N} \to_0 \mathbb{Q},\;\; \lvert \omega(x_c) \rvert > C \cdot p_m(x_c)\Bigr\} < \varepsilon.$$
The proof allocates $\varepsilon/8$ budget to the quadratic bound, derives the HS constant $C_{\mathrm{HS}}$ from the embedding $p_{m_0} \hookrightarrow p_{m_0+1}$, applies Gram-Schmidt per $N$, obtains a uniform tail bound $R$ via [`tail_bound_uniform`](../../Minlos/MinlosConcentration.lean#L1232), bounds the kernel contribution via [`kernel_concentration_bound`](../../Minlos/MinlosConcentration.lean#L1015), combines them via [`badSetN_bound_with_kernel`](../../Minlos/MinlosConcentration.lean#L1608), and lifts from per-$N$ to the full bad set via [`concentrationBadSet_measure_le`](../../Minlos/MinlosConcentration.lean#L456).

**Proof uses**: [`cf_norm_le_one`](../../Minlos/MinlosConcentration.lean#L86), [`combined_quadratic_bound`](../../Minlos/MinlosConcentration.lean#L189), [`gram_schmidt_seminorm`](../../Minlos/MinlosConcentration.lean#L690), [`tail_bound_uniform`](../../Minlos/MinlosConcentration.lean#L1232), [`kernel_concentration_bound`](../../Minlos/MinlosConcentration.lean#L1015), [`badSetN_bound_with_kernel`](../../Minlos/MinlosConcentration.lean#L1608), [`concentrationBadSet_measure_le`](../../Minlos/MinlosConcentration.lean#L456)

---

## Main theorem (wrapper)

### [`minlos_concentration`](../../Minlos/MinlosConcentration.lean#L1814) — Theorem

**Statement**: Same statement as `nuclear_cylindrical_concentration`. Convenience wrapper that applies it directly.

**Proof uses**: [`nuclear_cylindrical_concentration`](../../Minlos/MinlosConcentration.lean#L1672)

---

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