# `PietschBridge.lean` — Informal Summary

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

## Overview

Proves that a locally convex space satisfying Pietsch's nuclear dominance condition (every continuous seminorm is dominated by a nuclear expansion) is `IsHilbertNuclear` in the sense required by Bochner/Minlos (Hilbertian seminorms with Hilbert-Schmidt embeddings between consecutive levels). The proof constructs a **Hilbertian lift** from nuclear expansions, establishes a **Bessel inequality** for bounded functionals on Hilbertian seminorms, and builds a recursive family of Hilbertian seminorms via a **double Pietsch** construction.

## Status
**Main result**: [`isHilbertNuclear_of_nuclear`](../../Minlos/PietschBridge.lean#L806) -- Pietsch nuclearity implies `IsHilbertNuclear`
**Length**: 823 lines, 5 definition(s) + 32 theorem(s)/lemma(s)

---

### `IsNuclear` (definition, [L45](../../Minlos/PietschBridge.lean#L45))

```lean
def IsNuclear (E : Type*) [AddCommGroup E] [Module ℝ E]
    [TopologicalSpace E] : Prop
```

A locally convex TVS is **Pietsch nuclear** if for every continuous seminorm $p$, there exist continuous linear functionals $f_n$, non-negative reals $c_n$ with $\sum c_n < \infty$, and a continuous seminorm $q \ge p$ such that $\lvert f_n(x) \rvert \le q(x)$ for all $n, x$ and $p(x) \le \sum_n \lvert f_n(x) \rvert \cdot c_n$.

---

### `summable_sq_mul_of_bounded` (lemma, [L58](../../Minlos/PietschBridge.lean#L58))

If $\lvert f_n(x) \rvert \le q(x)$ for all $n$ and $\sum c_n < \infty$ with $c_n \ge 0$, then the series $\sum_n f_n(x)^2 \cdot c_n$ converges for each $x$, dominated by $q(x)^2 \cdot \sum c_n$.

**Dependencies**: `Summable.of_nonneg_of_le`, `sq_le_sq'`, `Summable.mul_left`

---

### `tsum_sq_mul_nonneg` (lemma, [L75](../../Minlos/PietschBridge.lean#L75))

$\sum_n f_n(x)^2 \cdot c_n \ge 0$ when $c_n \ge 0$.

**Dependencies**: `tsum_nonneg`

---

### `hilbertianLift` (definition, [L86](../../Minlos/PietschBridge.lean#L86))

```lean
def hilbertianLift (f : ℕ → (E →L[ℝ] ℝ)) (c : ℕ → ℝ)
    (hc_nn : ∀ n, 0 ≤ c n) (hc_sum : Summable c)
    (q : Seminorm ℝ E) (hfq : ∀ n x, |f n x| ≤ q x) : Seminorm ℝ E
```

The **Hilbertian lift** of a nuclear expansion: $r(x) = \sqrt{\sum_k f_k(x)^2 \cdot c_k}$. This is a seminorm satisfying the parallelogram law. The triangle inequality is proved via Minkowski's inequality for weighted $\ell^2$; homogeneity uses linearity of the $f_k$.

**Dependencies**: `Seminorm.of`, [`summable_sq_mul_of_bounded`](../../Minlos/PietschBridge.lean#L58), [`tsum_sq_mul_nonneg`](../../Minlos/PietschBridge.lean#L75), `Real.sum_mul_le_sqrt_mul_sqrt`

---

### `hilbertianLift_apply` (theorem, [L170](../../Minlos/PietschBridge.lean#L170))

The Hilbertian lift evaluates as $r(x) = \sqrt{\sum_k f_k(x)^2 \cdot c_k}$.

**Dependencies**: [`hilbertianLift`](../../Minlos/PietschBridge.lean#L86) (definitional)

---

### `hilbertianLift_isHilbertian` (theorem, [L180](../../Minlos/PietschBridge.lean#L180))

The Hilbertian lift satisfies the parallelogram law: $r(x+y)^2 + r(x-y)^2 = 2(r(x)^2 + r(y)^2)$. Proof: the identity $f_n(x+y)^2 + f_n(x-y)^2 = 2(f_n(x)^2 + f_n(y)^2)$ holds termwise by linearity of $f_n$, then sum and take square roots.

**Dependencies**: [`hilbertianLift_apply`](../../Minlos/PietschBridge.lean#L170), [`summable_sq_mul_of_bounded`](../../Minlos/PietschBridge.lean#L58), [`tsum_sq_mul_nonneg`](../../Minlos/PietschBridge.lean#L75)

---

### `hilbertianLift_dominates` (theorem, [L203](../../Minlos/PietschBridge.lean#L203))

Cauchy-Schwarz bound: $\sum_k \lvert f_k(x) \rvert \cdot c_k \le \sqrt{\sum_k c_k} \cdot r(x)$. Proved by applying finite Cauchy-Schwarz to partial sums and passing to the tsum limit.

**Dependencies**: [`hilbertianLift_apply`](../../Minlos/PietschBridge.lean#L170), [`summable_sq_mul_of_bounded`](../../Minlos/PietschBridge.lean#L58), `Real.sum_mul_le_sqrt_mul_sqrt`, `Real.tsum_le_of_sum_le`

---

### `hilbertianLift_le_dominator` (theorem, [L241](../../Minlos/PietschBridge.lean#L241))

The Hilbertian lift is bounded by the dominating seminorm: $r(x) \le \sqrt{\sum_k c_k} \cdot q(x)$. Proof: $\sum f_k(x)^2 c_k \le \sum q(x)^2 c_k = q(x)^2 \sum c_k$, take square root.

**Dependencies**: [`hilbertianLift_apply`](../../Minlos/PietschBridge.lean#L170), [`summable_sq_mul_of_bounded`](../../Minlos/PietschBridge.lean#L58)

---

### `R_congr'` (private lemma, [L272](../../Minlos/PietschBridge.lean#L272))

If $x = y$ then $R(x) = R(y)$ for a seminorm $R$. Helper for rewriting under the seminorm.

---

### `Seminorm.innerProd_self` (lemma, [L276](../../Minlos/PietschBridge.lean#L276))

$\mathrm{ip}(x, x) = R(x)^2$ for the polarization inner product of a seminorm $R$.

**Dependencies**: `Seminorm.innerProd`

---

### `Seminorm.innerProd_comm` (lemma, [L284](../../Minlos/PietschBridge.lean#L284))

Symmetry: $\mathrm{ip}(x, y) = \mathrm{ip}(y, x)$.

**Dependencies**: `Seminorm.innerProd`, `map_neg_eq_map`

---

### `Seminorm.innerProd_neg_left` (lemma, [L294](../../Minlos/PietschBridge.lean#L294))

$\mathrm{ip}(-x, y) = -\mathrm{ip}(x, y)$.

**Dependencies**: `Seminorm.innerProd`, `map_neg_eq_map`

---

### `Seminorm.innerProd_add_left` (lemma, [L308](../../Minlos/PietschBridge.lean#L308))

Additivity from the parallelogram law: if $R$ is Hilbertian then $\mathrm{ip}(x_1 + x_2, y) = \mathrm{ip}(x_1, y) + \mathrm{ip}(x_2, y)$. Uses four applications of the parallelogram identity with different argument pairs, combined by linear arithmetic.

**Dependencies**: `Seminorm.IsHilbertian`, [`R_congr'`](../../Minlos/PietschBridge.lean#L272), `map_neg_eq_map`

---

### `Seminorm.innerProd_sum_left` (lemma, [L325](../../Minlos/PietschBridge.lean#L325))

Finite-sum extension: $\mathrm{ip}\bigl(\sum_j x_j,\, y\bigr) = \sum_j \mathrm{ip}(x_j, y)$. Proved by induction on the finset using [`Seminorm.innerProd_add_left`](../../Minlos/PietschBridge.lean#L308).

**Dependencies**: [`Seminorm.innerProd_add_left`](../../Minlos/PietschBridge.lean#L308)

---

### `Seminorm.continuous_smul_add` (private lemma, [L334](../../Minlos/PietschBridge.lean#L334))

The map $t \mapsto R(t \cdot x + y)$ is continuous $\mathbb{R} \to \mathbb{R}$, with Lipschitz constant $R(x)$.

**Dependencies**: `Metric.continuous_iff`, `abs_sub_map_le_sub`, `map_smul_eq_mul`

---

### `Seminorm.innerProd_smul_left` (lemma, [L360](../../Minlos/PietschBridge.lean#L360))

Real homogeneity: $\mathrm{ip}(a \cdot x, y) = a \cdot \mathrm{ip}(x, y)$ for $a \in \mathbb{R}$. Proof: $t \mapsto \mathrm{ip}(t \cdot x, y)$ is an additive continuous function $\mathbb{R} \to \mathbb{R}$, hence $\mathbb{R}$-linear by `map_real_smul`.

**Dependencies**: [`Seminorm.innerProd_add_left`](../../Minlos/PietschBridge.lean#L308), [`Seminorm.continuous_smul_add`](../../Minlos/PietschBridge.lean#L334), `map_real_smul`

---

### `Seminorm.sq_add_of_innerProd_eq_zero` (private lemma, [L380](../../Minlos/PietschBridge.lean#L380))

Pythagorean theorem: if $\mathrm{ip}(x, y) = 0$ then $R(x+y)^2 = R(x)^2 + R(y)^2$.

**Dependencies**: `Seminorm.IsHilbertian`, `Seminorm.innerProd`

---

### `R_orthonormal_norm` (private lemma, [L389](../../Minlos/PietschBridge.lean#L389))

$R(v_j) = 1$ for each element of an $R$-orthonormal sequence.

**Dependencies**: `Seminorm.IsOrthonormalSeq`, [`Seminorm.innerProd_self`](../../Minlos/PietschBridge.lean#L276)

---

### `Seminorm.sq_sum_orthonormal` (lemma, [L396](../../Minlos/PietschBridge.lean#L396))

For an $R$-orthonormal sequence $\{v_j\}$: $R\bigl(\sum_j a_j v_j\bigr)^2 = \sum_j a_j^2$. Proved by induction on the number of vectors, using the Pythagorean theorem at each step.

**Dependencies**: [`Seminorm.sq_add_of_innerProd_eq_zero`](../../Minlos/PietschBridge.lean#L380), [`Seminorm.innerProd_sum_left`](../../Minlos/PietschBridge.lean#L325), [`Seminorm.innerProd_smul_left`](../../Minlos/PietschBridge.lean#L360), [`Seminorm.innerProd_comm`](../../Minlos/PietschBridge.lean#L284), [`R_orthonormal_norm`](../../Minlos/PietschBridge.lean#L389)

---

### `bessel_hilbertian` (theorem, [L433](../../Minlos/PietschBridge.lean#L433))

**Bessel inequality** for bounded functionals on Hilbertian seminorms. If $R$ is Hilbertian and $\varphi : E \to_L \mathbb{R}$ satisfies $\lvert \varphi(x) \rvert \le R(x)$, then for any finite $R$-orthonormal sequence $\{e_j\}_{j=1}^N$, $\sum_j \varphi(e_j)^2 \le 1$.

Proof: set $w = \sum_j \varphi(v_j) \cdot v_j$. By orthonormality $R(w)^2 = \sum_j \varphi(v_j)^2 = S$; by linearity $\varphi(w) = S$; and $S \le \lvert \varphi(w) \rvert \le R(w) = \sqrt{S}$, giving $S \le 1$.

**Dependencies**: [`Seminorm.sq_sum_orthonormal`](../../Minlos/PietschBridge.lean#L396)

---

### `isHilbertSchmidtEmbedding_of_nuclear` (theorem, [L459](../../Minlos/PietschBridge.lean#L459))

If $R$ is Hilbertian, $p \le R$ pointwise, and $p(x) \le \sum_k \lvert f_k(x) \rvert c_k$ with $\lvert f_k(x) \rvert \le R(x)$, then the inclusion $\hat{E}_R \to \hat{E}_p$ is **Hilbert-Schmidt**. The HS bound is $\sum_j p(e_j)^2 \le (\sum_k c_k)^2$ for any $R$-orthonormal $\{e_j\}$, proved by Cauchy-Schwarz + sum-swap + Bessel.

**Dependencies**: [`hilbertianLift_dominates`](../../Minlos/PietschBridge.lean#L203), [`bessel_hilbertian`](../../Minlos/PietschBridge.lean#L433), [`summable_sq_mul_of_bounded`](../../Minlos/PietschBridge.lean#L58), `Seminorm.IsHilbertSchmidtEmbedding`

---

### `nuclear_le_sumC_mul_Q` (private lemma, [L541](../../Minlos/PietschBridge.lean#L541))

Bound a nuclear sum by the product of total weight and dominating seminorm: $\sum_n \lvert F_n(x) \rvert C_n \le (\sum_n C_n) \cdot Q(x)$ when $\lvert F_n(x) \rvert \le Q(x)$.

**Dependencies**: `Summable.tsum_mono`, `Summable.mul_left`

---

### `hilbertian_smul` (private lemma, [L554](../../Minlos/PietschBridge.lean#L554))

Scaling a Hilbertian seminorm by $K \in \mathbb{R}_{\ge 0}$ preserves the parallelogram law.

**Dependencies**: `Seminorm.IsHilbertian`

---

### `doublePietsch_step` (private lemma, [L571](../../Minlos/PietschBridge.lean#L571))

**Double Pietsch step**: applies [`IsNuclear`](../../Minlos/PietschBridge.lean#L45) twice to a continuous seminorm $p$ to produce a Hilbertian seminorm $r \ge p$ together with a nuclear expansion whose functionals are bounded by $r$ (not just by some auxiliary $q$). The construction applies Pietsch to $p$ getting $(Q_A, F_A, C_A)$, then to $Q_A$ getting $(Q_B, G, D)$, builds the Hilbertian lift $R$ from $(G, D, Q_B)$, and sets $r = K \cdot R$ where $K = \max(\sum C_A, 1) \cdot \sqrt{\sum D}$.

**Dependencies**: [`IsNuclear`](../../Minlos/PietschBridge.lean#L45), [`hilbertianLift`](../../Minlos/PietschBridge.lean#L86), [`hilbertianLift_isHilbertian`](../../Minlos/PietschBridge.lean#L180), [`hilbertianLift_dominates`](../../Minlos/PietschBridge.lean#L203), [`hilbertianLift_le_dominator`](../../Minlos/PietschBridge.lean#L241), [`hilbertian_smul`](../../Minlos/PietschBridge.lean#L554), [`nuclear_le_sumC_mul_Q`](../../Minlos/PietschBridge.lean#L541)

---

### `seminorm_continuous_sup` (private theorem, [L639](../../Minlos/PietschBridge.lean#L639))

If seminorms $p$ and $q$ are continuous, then $p \sqcup q$ is continuous.

**Dependencies**: `Seminorm.sup_apply`, `Continuous.sup`

---

### `buildHilbertianBundle` (private definition, [L646](../../Minlos/PietschBridge.lean#L646))

```lean
private noncomputable def buildHilbertianBundle ...
    (n : ℕ) → { r : Seminorm ℝ E // Continuous r }
```

Bundled recursive construction: at step 0, applies [`doublePietsch_step`](../../Minlos/PietschBridge.lean#L571) to $q_0(0)$; at step $n+1$, applies it to $\mathrm{prev} \sqcup q_0(n+1)$. Returns a subtype carrying a continuity proof for use in the next step.

---

### `buildHilbertianFamily` (private definition, [L661](../../Minlos/PietschBridge.lean#L661))

```lean
private noncomputable def buildHilbertianFamily ... : ℕ → Seminorm ℝ E
```

Extracts the seminorm from [`buildHilbertianBundle`](../../Minlos/PietschBridge.lean#L646), giving the recursive Hilbertian family $r(n)$.

---

### `buildInput` (private abbreviation, [L669](../../Minlos/PietschBridge.lean#L669))

```lean
private noncomputable abbrev buildInput ... (n : ℕ) : Seminorm ℝ E
```

The sup input at step $n+1$: $r(n) \sqcup q_0(n+1)$.

---

### `buildInput_continuous` (private theorem, [L676](../../Minlos/PietschBridge.lean#L676))

The input $r(n) \sqcup q_0(n+1)$ is continuous.

**Dependencies**: [`seminorm_continuous_sup`](../../Minlos/PietschBridge.lean#L639), [`buildHilbertianBundle`](../../Minlos/PietschBridge.lean#L646)

---

### `buildHilbertianFamily_isHilbertian` (private theorem, [L684](../../Minlos/PietschBridge.lean#L684))

Each family member $r(n)$ satisfies the parallelogram law.

**Dependencies**: [`doublePietsch_step`](../../Minlos/PietschBridge.lean#L571), [`buildInput_continuous`](../../Minlos/PietschBridge.lean#L676)

---

### `buildHilbertianFamily_continuous` (private theorem, [L696](../../Minlos/PietschBridge.lean#L696))

Each family member $r(n)$ is continuous.

**Dependencies**: [`buildHilbertianBundle`](../../Minlos/PietschBridge.lean#L646)

---

### `buildFamily_stepSucc_spec` (private theorem, [L704](../../Minlos/PietschBridge.lean#L704))

The full `doublePietsch_step` specification at step $n+1$: $r(n+1)$ is continuous, Hilbertian, dominates $r(n) \sqcup q_0(n+1)$, and has a nuclear expansion with functionals bounded by $r(n+1)$.

**Dependencies**: [`doublePietsch_step`](../../Minlos/PietschBridge.lean#L571), [`buildInput_continuous`](../../Minlos/PietschBridge.lean#L676)

---

### `buildHilbertianFamily_dominates_q₀` (private theorem, [L720](../../Minlos/PietschBridge.lean#L720))

$q_0(n)(x) \le r(n)(x)$ pointwise: each original seminorm is dominated by its family member.

**Dependencies**: [`doublePietsch_step`](../../Minlos/PietschBridge.lean#L571), [`buildFamily_stepSucc_spec`](../../Minlos/PietschBridge.lean#L704)

---

### `buildHilbertianFamily_monotone` (private theorem, [L735](../../Minlos/PietschBridge.lean#L735))

$r(n)(x) \le r(n+1)(x)$ pointwise: the family is monotone increasing.

**Dependencies**: [`buildFamily_stepSucc_spec`](../../Minlos/PietschBridge.lean#L704)

---

### `buildHilbertianFamily_hs` (private theorem, [L749](../../Minlos/PietschBridge.lean#L749))

Consecutive family members have **Hilbert-Schmidt embeddings**: the inclusion $\hat{E}_{r(n+1)} \to \hat{E}_{r(n)}$ is Hilbert-Schmidt.

**Dependencies**: [`buildFamily_stepSucc_spec`](../../Minlos/PietschBridge.lean#L704), [`isHilbertSchmidtEmbedding_of_nuclear`](../../Minlos/PietschBridge.lean#L459), [`buildHilbertianFamily_monotone`](../../Minlos/PietschBridge.lean#L735)

---

### `buildHilbertianFamily_withSeminorms` (private theorem, [L776](../../Minlos/PietschBridge.lean#L776))

The Hilbertian family $\{r(n)\}$ generates the same topology as the original family $\{q_0(n)\}$. Uses `WithSeminorms.congr`: the two families are mutually bounded since $q_0(n) \le r(n)$ and each $r(n)$ is continuous in the $q_0$-topology.

**Dependencies**: `WithSeminorms.congr`, `Seminorm.bound_of_continuous`, [`buildHilbertianFamily_dominates_q₀`](../../Minlos/PietschBridge.lean#L720), [`buildHilbertianFamily_continuous`](../../Minlos/PietschBridge.lean#L696)

---

### `isHilbertNuclear_of_nuclear` (theorem, [L806](../../Minlos/PietschBridge.lean#L806))

**Main theorem**: Pietsch nuclearity implies `IsHilbertNuclear`. Given `IsNuclear E` and a generating family of seminorms $q_0$ with `WithSeminorms q_0$, constructs the recursive Hilbertian family $r(n)$ and verifies:
1. Each $r(n)$ is Hilbertian ([`buildHilbertianFamily_isHilbertian`](../../Minlos/PietschBridge.lean#L684)),
2. $\{r(n)\}$ generates the topology ([`buildHilbertianFamily_withSeminorms`](../../Minlos/PietschBridge.lean#L776)),
3. Consecutive members have HS embeddings ([`buildHilbertianFamily_hs`](../../Minlos/PietschBridge.lean#L749)).

**Dependencies**: [`buildHilbertianFamily`](../../Minlos/PietschBridge.lean#L661), [`buildHilbertianFamily_isHilbertian`](../../Minlos/PietschBridge.lean#L684), [`buildHilbertianFamily_withSeminorms`](../../Minlos/PietschBridge.lean#L776), [`buildHilbertianFamily_hs`](../../Minlos/PietschBridge.lean#L749), `IsHilbertNuclear`

---

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