# `SazonovTightness.lean` — Informal Summary

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

## Overview

This file establishes that Sazonov-continuous characteristic functions imply
uniform tightness of finite-dimensional marginal measures. The proof proceeds
via Gaussian averaging: a Fubini exchange relates the Gaussian-weighted
integral of $\mathrm{Re}(1-\varphi)$ to the exponential moment
$\mathbb{E}[1-e^{-\sigma^2\lVert y\rVert^2/2}]$, a spectral decomposition
bounds the Gaussian second moment $\mathbb{E}_\gamma[\langle x,Sx\rangle]$ by
$\sigma^2\,\mathrm{Tr}(S)$, and a Chebyshev-type tail bound converts the
exponential moment into a mass estimate on $\{\lVert y\rVert \ge R\}$.

## Status

**Main result**: `sazonov_tightness` — Sazonov CF continuity implies uniform tightness of all finite-dimensional marginals.
**Length**: 1094 lines, 6 definition(s) + 34 theorem(s)/lemma(s)

---

### `SazonovContinuousAt` (def, L44)

[`SazonovContinuousAt`](../../Minlos/SazonovTightness.lean#L44)

```lean
def SazonovContinuousAt (φ : H → ℂ) :=
  ∀ ε > 0, ∃ S : SazonovIndex H,
    ∀ x : H, quadForm S.op x < 1 → ‖1 - φ x‖ < ε
```

Sazonov continuity at zero: for every $\varepsilon > 0$ there exists a positive
trace-class operator $S$ such that $\langle x, Sx\rangle < 1$ implies
$\lvert 1 - \varphi(x)\rvert < \varepsilon$.

---

### `marginalFun` (def, L52)

[`marginalFun`](../../Minlos/SazonovTightness.lean#L52)

```lean
def marginalFun (φ : H → ℂ) {n : ℕ} (v : Fin n → H) :
    EuclideanSpace ℝ (Fin n) → ℂ
```

For a family $v : \mathrm{Fin}\,n \to H$, the marginal characteristic function
$\varphi_v(t) = \varphi\bigl(\sum_i t_i\, v_i\bigr)$.

---

### `marginalFun_isPositiveDefinite` (lemma, L58)

[`marginalFun_isPositiveDefinite`](../../Minlos/SazonovTightness.lean#L58)

The marginal function of a positive-definite function is positive definite.
If $\varphi : H \to \mathbb{C}$ is positive definite and $v : \mathrm{Fin}\,n \to H$,
then $\varphi_v$ is positive definite on $\mathbb{R}^n$.

**Proof deps**: `isPositiveDefinite_precomp_linear` from [`Bochner/PositiveDefinite.lean`](../../Bochner/PositiveDefinite.lean).

---

### `one_sub_exp_neg_pos` (lemma, L77)

[`one_sub_exp_neg_pos`](../../Minlos/SazonovTightness.lean#L77)

For $t > 0$, $1 - e^{-t} > 0$.

**Proof deps**: `Real.exp_strictMono`, `Real.exp_zero`.

---

### `exp_neg_le_exp_neg` (lemma, L84)

[`exp_neg_le_exp_neg`](../../Minlos/SazonovTightness.lean#L84)

If $a \le b$ then $e^{-b} \le e^{-a}$.

**Proof deps**: `Real.exp_le_exp_of_le`.

---

### `one_sub_exp_half_sq_pos` (lemma, L89)

[`one_sub_exp_half_sq_pos`](../../Minlos/SazonovTightness.lean#L89)

For $R > 0$, the denominator $1 - e^{-R^2/2} > 0$.

**Proof deps**: `one_sub_exp_neg_pos`.

---

### `tail_bound_from_exp_integral` (lemma, L95)

[`tail_bound_from_exp_integral`](../../Minlos/SazonovTightness.lean#L95)

Chebyshev/Markov bound with Gaussian scaling: if
$\int (1 - e^{-\sigma^2\lVert y\rVert^2/2})\,d\mu \le C$, then
$\mu(\{\lVert y\rVert \ge R\}) \le C / (1 - e^{-\sigma^2 R^2/2})$.

**Proof deps**: Mathlib measure theory (`setIntegral_mono_on`, `setIntegral_le_integral`).

---

### `gaussDensity` (abbrev, L157)

[`gaussDensity`](../../Minlos/SazonovTightness.lean#L157)

```lean
abbrev gaussDensity (σ : ℝ) (x : V) : ℝ :=
  Real.exp (-(1 / (2 * σ ^ 2)) * ‖x‖ ^ 2)
```

The (un-normalized) Gaussian density $\exp\bigl(-\lVert x\rVert^2/(2\sigma^2)\bigr)$.

---

### `gaussDensity_nonneg'` (lemma, L162)

[`gaussDensity_nonneg'`](../../Minlos/SazonovTightness.lean#L162)

$\mathrm{gaussDensity}\;\sigma\;x \ge 0$.

**Proof deps**: `Real.exp_nonneg`.

---

### `gaussDensity_continuous'` (lemma, L167)

[`gaussDensity_continuous'`](../../Minlos/SazonovTightness.lean#L167)

$x \mapsto \mathrm{gaussDensity}\;\sigma\;x$ is continuous.

**Proof deps**: `fun_prop`.

---

### `gaussDensity_integrable'` (lemma, L171)

[`gaussDensity_integrable'`](../../Minlos/SazonovTightness.lean#L171)

For $\sigma > 0$, $\mathrm{gaussDensity}\;\sigma$ is integrable with respect to Lebesgue measure.

**Proof deps**: `GaussianFourier.integrable_cexp_neg_mul_sq_norm_add`.

---

### `gaussDensity_integral_pos'` (lemma, L186)

[`gaussDensity_integral_pos'`](../../Minlos/SazonovTightness.lean#L186)

For $\sigma > 0$, $\int \mathrm{gaussDensity}\;\sigma\;x\,dx > 0$.

**Proof deps**: `integral_pos_of_integrable_nonneg_nonzero`, `gaussDensity_integrable'`, `gaussDensity_nonneg'`.

---

### `gaussian_fourier_eq'` (private lemma, L194)

[`gaussian_fourier_eq'`](../../Minlos/SazonovTightness.lean#L194)

Fourier transform of the un-normalized Gaussian:
$\int e^{-\lVert x\rVert^2/(2\sigma^2)}\,e^{i\langle y,x\rangle}\,dx = C \cdot e^{-\sigma^2\lVert y\rVert^2/2}$
where $C = \int \mathrm{gaussDensity}\;\sigma$.

**Proof deps**: `GaussianFourier.integral_cexp_neg_mul_sq_norm_add`.

---

### `exp_neg_sq_integrable_prob'` (private lemma, L221)

[`exp_neg_sq_integrable_prob'`](../../Minlos/SazonovTightness.lean#L221)

$y \mapsto e^{-\sigma^2\lVert y\rVert^2/2}$ is integrable with respect to any probability measure.

**Proof deps**: Mathlib integrability (`Integrable.mono'`).

---

### `cexp_neg_sq_integrable_prob'` (private lemma, L232)

[`cexp_neg_sq_integrable_prob'`](../../Minlos/SazonovTightness.lean#L232)

Complex-valued version: $y \mapsto \exp(-\sigma^2\lVert y\rVert^2/2)$ is integrable (as $\mathbb{C}$-valued) w.r.t. any probability measure.

**Proof deps**: `exp_neg_sq_integrable_prob'`, `Integrable.ofReal`.

---

### `gaussDensity_mul_charFun_re_integrable'` (lemma, L240)

[`gaussDensity_mul_charFun_re_integrable'`](../../Minlos/SazonovTightness.lean#L240)

$x \mapsto \mathrm{gaussDensity}\;\sigma\;x \cdot \mathrm{Re}(\varphi(x))$ is integrable (Lebesgue), when $\varphi$ is the characteristic function of a probability measure.

**Proof deps**: `gaussDensity_integrable'`, `norm_charFun_le_one`.

---

### `gaussDensity_mul_charFun_integrable'` (private lemma, L255)

[`gaussDensity_mul_charFun_integrable'`](../../Minlos/SazonovTightness.lean#L255)

$x \mapsto \mathrm{gaussDensity}\;\sigma\;x \cdot \varphi(x)$ is integrable ($\mathbb{C}$-valued, Lebesgue).

**Proof deps**: `gaussDensity_integrable'`, `norm_charFun_le_one`.

---

### `fubini_gaussian_charFun` (theorem, L273)

[`fubini_gaussian_charFun`](../../Minlos/SazonovTightness.lean#L273)

**Fubini identity for Gaussian averaging.**
$$\int (1 - e^{-\sigma^2\lVert y\rVert^2/2})\,d\mu(y)
  = C^{-1}\!\int e^{-\lVert x\rVert^2/(2\sigma^2)}\,\mathrm{Re}(1-\varphi(x))\,dx$$
where $C = \int \mathrm{gaussDensity}\;\sigma$.

**Proof deps**: Fubini (`integral_integral_swap`), [`gaussian_fourier_eq'`](../../Minlos/SazonovTightness.lean#L194), `gaussDensity_mul_charFun_re_integrable'`, `Complex.reCLM.integral_comp_comm`.

---

### `gaussian_real_formula'` (private lemma, L351)

[`gaussian_real_formula'`](../../Minlos/SazonovTightness.lean#L351)

Real Gaussian integral with linear term:
$\int e^{-b\lVert x\rVert^2 + c\langle w,x\rangle}\,dx = (\int e^{-b\lVert x\rVert^2}\,dx)\cdot e^{c^2\lVert w\rVert^2/(4b)}$.

**Proof deps**: `GaussianFourier.integral_cexp_neg_mul_sq_norm_add`, `GaussianFourier.integral_cexp_neg_mul_sq_norm`.

---

### `id_le_sinh'` (private lemma, L371)

[`id_le_sinh'`](../../Minlos/SazonovTightness.lean#L371)

For $t \ge 0$, $t \le \sinh t$.

**Proof deps**: `monotoneOn_of_deriv_nonneg`, `Real.hasDerivAt_sinh`, `Real.one_le_cosh`.

---

### `half_sq_le_cosh_sub_one'` (private lemma, L386)

[`half_sq_le_cosh_sub_one'`](../../Minlos/SazonovTightness.lean#L386)

For all $x \in \mathbb{R}$, $x^2/2 \le \cosh x - 1$.

**Proof deps**: [`id_le_sinh'`](../../Minlos/SazonovTightness.lean#L371), `Real.cosh_two_mul`, `Real.cosh_sq`.

---

### `gaussDensity_mul_exp_inner_integrable'` (private lemma, L408)

[`gaussDensity_mul_exp_inner_integrable'`](../../Minlos/SazonovTightness.lean#L408)

$x \mapsto \mathrm{gaussDensity}\;\sigma\;x \cdot e^{c\langle w,x\rangle}$ is integrable.

**Proof deps**: `GaussianFourier.integrable_cexp_neg_mul_sq_norm_add`.

---

### `gaussDensity_exp_inner_integral'` (private lemma, L427)

[`gaussDensity_exp_inner_integral'`](../../Minlos/SazonovTightness.lean#L427)

$\int \mathrm{gaussDensity}\;\sigma\;x \cdot e^{c\langle w,x\rangle}\,dx = C \cdot e^{c^2\sigma^2\lVert w\rVert^2/2}$.

**Proof deps**: [`gaussian_real_formula'`](../../Minlos/SazonovTightness.lean#L351).

---

### `tendsto_exp_slope'` (private lemma, L440)

[`tendsto_exp_slope'`](../../Minlos/SazonovTightness.lean#L440)

$(e^{tA}-1)/t \to A$ as $t \to 0^+$.

**Proof deps**: `HasDerivAt.tendsto_slope_zero_right`, `Real.hasDerivAt_exp`.

---

### `gaussDensity_mul_cosh_integrable'` (private lemma, L455)

[`gaussDensity_mul_cosh_integrable'`](../../Minlos/SazonovTightness.lean#L455)

$x \mapsto \mathrm{gaussDensity}\;\sigma\;x \cdot \cosh(c\langle w,x\rangle)$ is integrable.

**Proof deps**: [`gaussDensity_mul_exp_inner_integrable'`](../../Minlos/SazonovTightness.lean#L408).

---

### `gaussDensity_cosh_integral'` (private lemma, L473)

[`gaussDensity_cosh_integral'`](../../Minlos/SazonovTightness.lean#L473)

$\int \mathrm{gaussDensity}\;\sigma\;x \cdot \cosh(c\langle w,x\rangle)\,dx = C \cdot e^{c^2\sigma^2\lVert w\rVert^2/2}$.

**Proof deps**: [`gaussDensity_exp_inner_integral'`](../../Minlos/SazonovTightness.lean#L427).

---

### `gaussDensity_mul_inner_sq_integrable'` (private lemma, L493)

[`gaussDensity_mul_inner_sq_integrable'`](../../Minlos/SazonovTightness.lean#L493)

$x \mapsto \mathrm{gaussDensity}\;\sigma\;x \cdot \langle w,x\rangle^2$ is integrable.

**Proof deps**: [`gaussDensity_mul_cosh_integrable'`](../../Minlos/SazonovTightness.lean#L455), [`half_sq_le_cosh_sub_one'`](../../Minlos/SazonovTightness.lean#L386).

---

### `gaussian_inner_sq_le'` (private lemma, L507)

[`gaussian_inner_sq_le'`](../../Minlos/SazonovTightness.lean#L507)

Gaussian second moment in one direction:
$\int \mathrm{gaussDensity}\;\sigma\;x \cdot \langle w,x\rangle^2\,dx \le C \cdot \sigma^2\lVert w\rVert^2$.
Proved by bounding above by $2C(e^{tA}-1)/t$ and taking the limit $t\to 0^+$.

**Proof deps**: [`gaussDensity_cosh_integral'`](../../Minlos/SazonovTightness.lean#L473), [`half_sq_le_cosh_sub_one'`](../../Minlos/SazonovTightness.lean#L386), [`tendsto_exp_slope'`](../../Minlos/SazonovTightness.lean#L440), `ge_of_tendsto`.

---

### `gaussian_quadForm_integral_le` (theorem, L557)

[`gaussian_quadForm_integral_le`](../../Minlos/SazonovTightness.lean#L557)

**Gaussian second moment bound via spectral decomposition.**
$$C^{-1}\!\int e^{-\lVert x\rVert^2/(2\sigma^2)}\,\langle x,Sx\rangle\,dx \;\le\; \sigma^2\,\mathrm{Tr}(S)$$
for $S \ge 0$ with trace bounded by $T$. Uses the eigenbasis of $S$ to decompose
$\langle x,Sx\rangle = \sum_i \lambda_i\langle e_i,x\rangle^2$, then applies the
one-direction bound to each term.

**Proof deps**: [`gaussian_inner_sq_le'`](../../Minlos/SazonovTightness.lean#L507), `LinearMap.IsPositive.eigenvectorBasis`, `LinearMap.IsPositive.eigenvalues`.

---

### `mul_exp_neg_le_one'` (private lemma, L627)

[`mul_exp_neg_le_one'`](../../Minlos/SazonovTightness.lean#L627)

For $t \ge 0$, $t\,e^{-t} \le 1$.

**Proof deps**: `Real.add_one_le_exp`.

---

### `gaussDensity_mul_quadForm_integrable'` (lemma, L632)

[`gaussDensity_mul_quadForm_integrable'`](../../Minlos/SazonovTightness.lean#L632)

$x \mapsto \mathrm{gaussDensity}\;\sigma\;x \cdot \langle x,Sx\rangle$ is integrable for any continuous linear operator $S$.

**Proof deps**: [`mul_exp_neg_le_one'`](../../Minlos/SazonovTightness.lean#L627), [`gaussDensity_integrable'`](../../Minlos/SazonovTightness.lean#L171), operator norm bound $\lvert\langle x,Sx\rangle\rvert \le \lVert S\rVert\lVert x\rVert^2$.

---

### `gaussian_averaging_bound` (theorem, L699)

[`gaussian_averaging_bound`](../../Minlos/SazonovTightness.lean#L699)

**The Gaussian averaging bound.**
$$\int \bigl(1 - e^{-\sigma^2\lVert y\rVert^2/2}\bigr)\,d\mu(y) \;\le\; \varepsilon + 2\sigma^2 T$$
given that $\langle x,Sx\rangle < 1 \Rightarrow \lVert 1-\varphi(x)\rVert < \varepsilon$
and $\mathrm{Tr}(S) \le T$. Combines the Fubini identity, the pointwise bound
$\mathrm{Re}(1-\varphi) \le \varepsilon + 2\langle x,Sx\rangle$, and the Gaussian
second moment estimate.

**Proof deps**: [`fubini_gaussian_charFun`](../../Minlos/SazonovTightness.lean#L273), [`gaussian_quadForm_integral_le`](../../Minlos/SazonovTightness.lean#L557), [`gaussDensity_mul_quadForm_integrable'`](../../Minlos/SazonovTightness.lean#L632).

---

### `scaled_tail_bound` (lemma, L789)

[`scaled_tail_bound`](../../Minlos/SazonovTightness.lean#L789)

Scaled Chebyshev bound combining Gaussian averaging with the exponential tail:
$$\mu(\{\lVert y\rVert \ge R\}) \;\le\; \frac{\varepsilon + 2\sigma^2 T}{1 - e^{-\sigma^2 R^2/2}}.$$

**Proof deps**: [`gaussian_averaging_bound`](../../Minlos/SazonovTightness.lean#L699), [`tail_bound_from_exp_integral`](../../Minlos/SazonovTightness.lean#L95).

---

### `embedON` (private def, L814)

[`embedON`](../../Minlos/SazonovTightness.lean#L814)

```lean
private def embedON {n : ℕ} (v : Fin n → H) : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] H
```

The embedding $t \mapsto \sum_i t_i\,v_i$ from $\mathbb{R}^n$ to $H$.

---

### `projON` (private def, L822)

[`projON`](../../Minlos/SazonovTightness.lean#L822)

```lean
private def projON {n : ℕ} (v : Fin n → H) : H →ₗ[ℝ] EuclideanSpace ℝ (Fin n)
```

The projection $x \mapsto (\langle v_i, x\rangle)_i$ from $H$ to $\mathbb{R}^n$.

---

### `restrictOp` (def, L830)

[`restrictOp`](../../Minlos/SazonovTightness.lean#L830)

```lean
def restrictOp (S : H →L[ℝ] H) {n : ℕ} (v : Fin n → H) :
    EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)
```

Restriction of $S$ to the subspace spanned by an orthonormal family $v$,
defined as $\pi \circ S \circ \iota$. In matrix form:
$(S_v)_{ij} = \langle v_i, S(v_j)\rangle$.

---

### `restrictOp_apply` (lemma, L836)

[`restrictOp_apply`](../../Minlos/SazonovTightness.lean#L836)

Coordinate formula: $(\mathrm{restrictOp}\;S\;v\;t)_i = \langle v_i,\, S(\sum_j t_j v_j)\rangle$.

**Proof deps**: definitions of `restrictOp`, `projON`, `embedON`.

---

### `restrictOp_quadForm` (lemma, L843)

[`restrictOp_quadForm`](../../Minlos/SazonovTightness.lean#L843)

The quadratic form of the restricted operator equals the original:
$\langle t,\,S_v\,t\rangle = \langle \sum_i t_i v_i,\, S(\sum_j t_j v_j)\rangle$.

**Proof deps**: [`restrictOp_apply`](../../Minlos/SazonovTightness.lean#L836), `sum_inner`.

---

### `inner_self_adjoint_comm` (private lemma, L854)

[`inner_self_adjoint_comm`](../../Minlos/SazonovTightness.lean#L854)

For a positive (hence self-adjoint) operator $S$:
$\langle a, Sb\rangle = \langle b, Sa\rangle$.

**Proof deps**: `ContinuousLinearMap.adjoint_inner_left`, `IsPositive.isSelfAdjoint`.

---

### `restrictOp_isPositive` (lemma, L861)

[`restrictOp_isPositive`](../../Minlos/SazonovTightness.lean#L861)

The restriction of a positive operator to an orthonormal family is positive.

**Proof deps**: [`inner_self_adjoint_comm`](../../Minlos/SazonovTightness.lean#L854), [`restrictOp_quadForm`](../../Minlos/SazonovTightness.lean#L843), `quadForm_nonneg`.

---

### `orthonormal_diag_le_hilbert_trace` (theorem, L886)

[`orthonormal_diag_le_hilbert_trace`](../../Minlos/SazonovTightness.lean#L886)

**Finite-diagonal $\le$ Hilbert trace.** For a positive operator $S$ with summable
Hilbert-basis trace, any finite orthonormal set $\{v_j\}$ satisfies
$$\sum_j \langle v_j, S v_j\rangle \;\le\; \sum_k^\infty \langle b_k, S b_k\rangle.$$
Proof: decompose $b_k = P(b_k) + Q(b_k)$ via orthogonal projection $P$ onto
$\mathrm{span}(v)$; the cross term vanishes by Parseval and orthonormality,
so the difference $= \sum_k \langle Q(b_k), S\,Q(b_k)\rangle \ge 0$.

**Proof deps**: `HilbertBasis.hasSum_inner_mul_inner`, `tsum_nonneg`.

---

### `restrictOp_trace_eq_diag` (lemma, L964)

[`restrictOp_trace_eq_diag`](../../Minlos/SazonovTightness.lean#L964)

The trace of $\mathrm{restrictOp}\;S\;v$ in any ONB of $\mathbb{R}^n$ equals
$\sum_j \langle v_j, S v_j\rangle$. Uses `LinearMap.trace_eq_sum_inner` for
basis independence on finite-dimensional Euclidean space.

**Proof deps**: `LinearMap.trace_eq_sum_inner`, `EuclideanSpace.basisFun`, [`restrictOp_apply`](../../Minlos/SazonovTightness.lean#L836).

---

### `restrictOp_trace_le` (lemma, L997)

[`restrictOp_trace_le`](../../Minlos/SazonovTightness.lean#L997)

The trace of the restricted operator is bounded by the Hilbert trace of the
original: for any ONB $b'$ of $\mathbb{R}^n$,
$\sum_i \langle b'_i, S_v b'_i\rangle \le \sum_k^\infty \langle b_k, S b_k\rangle$.

**Proof deps**: [`restrictOp_trace_eq_diag`](../../Minlos/SazonovTightness.lean#L964), [`orthonormal_diag_le_hilbert_trace`](../../Minlos/SazonovTightness.lean#L886).

---

### `exists_R_for_tail_bound` (lemma, L1013)

[`exists_R_for_tail_bound`](../../Minlos/SazonovTightness.lean#L1013)

For any $0 < C < \eta$ and $\sigma > 0$, there exists $R > 0$ such that
$C / (1 - e^{-\sigma^2 R^2/2}) < \eta$.

**Proof deps**: `Real.exp_log`, `Real.log_neg`.

---

### `sazonov_tightness` (theorem, L1039)

[`sazonov_tightness`](../../Minlos/SazonovTightness.lean#L1039)

**Sazonov Tightness Theorem.** If $\varphi : H \to \mathbb{C}$ is positive definite,
normalized ($\varphi(0)=1$), continuous, and Sazonov-continuous at $0$, then
the family of all finite-dimensional marginal measures is uniformly tight:
for every $\eta > 0$ there exists $R > 0$ such that for all $n$, all
orthonormal $v : \mathrm{Fin}\,n \to H$, and all probability measures $\mu$
on $\mathbb{R}^n$ with $\widehat{\mu} = \varphi_v$, one has
$\mu(\{\lVert y\rVert \ge R\}) < \eta$.

The proof chooses $\varepsilon = \eta/3$, obtains a Sazonov index $S$ with trace
$T$, sets $\sigma = \sqrt{\eta/(6(T+1))}$, verifies
$\varepsilon + 2\sigma^2 T < \eta$, restricts $S$ to each marginal subspace
(trace is bounded via `restrictOp_trace_le`), applies `gaussian_averaging_bound`
and `tail_bound_from_exp_integral`, and finds $R$ via `exists_R_for_tail_bound`.

**Proof deps**: [`gaussian_averaging_bound`](../../Minlos/SazonovTightness.lean#L699), [`tail_bound_from_exp_integral`](../../Minlos/SazonovTightness.lean#L95), [`restrictOp_isPositive`](../../Minlos/SazonovTightness.lean#L861), [`restrictOp_trace_le`](../../Minlos/SazonovTightness.lean#L997), [`exists_R_for_tail_bound`](../../Minlos/SazonovTightness.lean#L1013), `SazonovIndex.traceClass`.

---

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