# `Sazonov.lean` — Informal Summary

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

## Overview

This file defines the Sazonov topology on a real Hilbert space $H$, a locally convex topology generated by seminorms $x \mapsto \sqrt{\langle x, Sx \rangle}$ indexed by positive trace-class operators $S$. A function $\varphi : H \to \mathbb{C}$ is continuous in the Sazonov topology if for every $\varepsilon > 0$ there exists a positive trace-class operator $S$ such that $\lvert\varphi(x) - \varphi(y)\rvert < \varepsilon$ whenever $\sqrt{\langle x-y, S(x-y) \rangle} < 1$. Key lemmas establish Cauchy-Schwarz for the semi-inner product $\langle \cdot, S \cdot \rangle$ and the triangle inequality for the Sazonov seminorm.

## Status
**Main result**: Sazonov topology definition with supporting seminorm infrastructure, fully proven (0 sorries, 0 axioms).
**Length**: 193 lines, 6 definition(s)/structure(s) + 7 theorem(s)/lemma(s)

---

## Positive Trace-Class Operators

### [`IsPositiveTraceClass`](../../Bochner/Sazonov.lean#L51)

```
def IsPositiveTraceClass (S : H →L[ℝ] H) : Prop
```

An operator $S : H \to_{\mathbb{R}} H$ is positive trace-class if $S$ is positive (self-adjoint with $\langle x, Sx \rangle \geq 0$) and $\sum_i \langle e_i, S e_i \rangle$ converges for some Hilbert basis $\{e_i\}$ (basis-independent for positive operators).

---

## Quadratic Form and Seminorm

### [`quadForm`](../../Bochner/Sazonov.lean#L59)

```
def quadForm (S : H →L[ℝ] H) (x : H) : ℝ
```

The quadratic form associated to an operator $S$: $x \mapsto \langle x, Sx \rangle$.

---

### [`star_real`](../../Bochner/Sazonov.lean#L65) *(private)*

For $a : \mathbb{R}$, the star-ring endomorphism acts as the identity: $\overline{a} = a$.

---

### [`quadForm_nonneg`](../../Bochner/Sazonov.lean#L69)

If $S$ is positive, then $\langle x, Sx \rangle \geq 0$ for all $x$.

Proof uses: `ContinuousLinearMap.IsPositive.re_inner_nonneg_left`, `real_inner_comm`.

---

### [`inner_S_smul_right`](../../Bochner/Sazonov.lean#L75)

$\langle x, S(t \cdot y) \rangle = t \cdot \langle x, Sy \rangle$ (linearity in scalar multiplication on the right).

Proof uses: `ContinuousLinearMap.map_smul`, `inner_smul_right`.

---

### [`quadForm_smul`](../../Bochner/Sazonov.lean#L79)

$\mathrm{quadForm}\; S\; (t \cdot x) = t^2 \cdot \mathrm{quadForm}\; S\; x$ (homogeneity of degree 2).

Proof uses: `ContinuousLinearMap.map_smul`, `inner_smul_left`, `inner_smul_right`.

---

### [`quadForm_add`](../../Bochner/Sazonov.lean#L84)

$\langle x+y, S(x+y) \rangle = \langle x, Sx \rangle + 2\langle x, Sy \rangle + \langle y, Sy \rangle$ (polarization identity).

Proof uses: bilinearity of inner product, self-adjointness of $S$ (via `ContinuousLinearMap.IsPositive.inner_left_eq_inner_right` giving $\langle y, Sx \rangle = \langle x, Sy \rangle$).

---

### [`inner_sq_le_quadForm_mul`](../../Bochner/Sazonov.lean#L96)

If $S$ is positive, then $\langle x, Sy \rangle^2 \leq \langle x, Sx \rangle \cdot \langle y, Sy \rangle$ (Cauchy-Schwarz for the semi-inner product $\langle \cdot, S \cdot \rangle$).

Proof uses: the quadratic $t \mapsto \langle x + ty, S(x + ty) \rangle \geq 0$ for all $t$, so its discriminant is nonpositive. Cases on whether $\langle y, Sy \rangle = 0$ or positive. Depends on [`quadForm_nonneg`](../../Bochner/Sazonov.lean#L69), [`quadForm_add`](../../Bochner/Sazonov.lean#L84), [`inner_S_smul_right`](../../Bochner/Sazonov.lean#L75), [`quadForm_smul`](../../Bochner/Sazonov.lean#L79).

---

### [`sqrt_quadForm_add_le`](../../Bochner/Sazonov.lean#L140)

$\sqrt{\langle x+y, S(x+y) \rangle} \leq \sqrt{\langle x, Sx \rangle} + \sqrt{\langle y, Sy \rangle}$ (triangle inequality for the Sazonov seminorm).

Proof uses: [`quadForm_nonneg`](../../Bochner/Sazonov.lean#L69) for nonnegativity, [`inner_sq_le_quadForm_mul`](../../Bochner/Sazonov.lean#L96) to bound the cross term, [`quadForm_add`](../../Bochner/Sazonov.lean#L84) to expand, `Real.sqrt_le_sqrt`, `Real.le_sqrt_of_sq_le`.

---

### [`sazonovSeminorm`](../../Bochner/Sazonov.lean#L161)

```
def sazonovSeminorm (S : H →L[ℝ] H) (hS : S.IsPositive) : Seminorm ℝ H
```

The Sazonov seminorm for a positive operator $S$: $x \mapsto \sqrt{\langle x, Sx \rangle}$. This is a seminorm because it maps $0$ to $0$, is subadditive (by [`sqrt_quadForm_add_le`](../../Bochner/Sazonov.lean#L140)), is negation-invariant, and is absolutely homogeneous ($p(a \cdot x) = \lvert a \rvert \cdot p(x)$, via [`quadForm_smul`](../../Bochner/Sazonov.lean#L79) and `Real.sqrt_sq_eq_abs`).

---

## Sazonov Topology

### [`SazonovIndex`](../../Bochner/Sazonov.lean#L176)

```
structure SazonovIndex (H : Type u) [NormedAddCommGroup H] [InnerProductSpace ℝ H]
    [CompleteSpace H]
```

The index type for the Sazonov seminorm family: bundles a continuous linear operator `op : H →L[ℝ] H` with proofs that it is positive (`pos`) and positive trace-class (`traceClass`).

---

### [`sazonovFamily`](../../Bochner/Sazonov.lean#L183)

```
def sazonovFamily (H : Type u) [NormedAddCommGroup H] [InnerProductSpace ℝ H]
    [CompleteSpace H] : SeminormFamily ℝ H (SazonovIndex H)
```

The Sazonov seminorm family indexed by `SazonovIndex H`: maps each positive trace-class operator $S$ to the seminorm $x \mapsto \sqrt{\langle x, Sx \rangle}$ via [`sazonovSeminorm`](../../Bochner/Sazonov.lean#L161).

---

### [`sazonovTopology`](../../Bochner/Sazonov.lean#L189)

```
def sazonovTopology (H : Type u) [NormedAddCommGroup H] [InnerProductSpace ℝ H]
    [CompleteSpace H] : TopologicalSpace H
```

The Sazonov topology on $H$: the locally convex topology generated by [`sazonovFamily`](../../Bochner/Sazonov.lean#L183) via the module filter basis construction.

---

*This file has **6** definitions/structures and **7** theorems/lemmas (0 with sorry).*