# `Support.lean` — Informal Summary

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

## Overview

Characterizes the support of the Gaussian measure $\mu_T$ on the weak dual $E'$.
The measure is supported on configurations with finite basis norm
($\sum_n \lvert\omega(e_n)\rvert^2 < \infty$) when $T$ is Hilbert–Schmidt.
Defines the Cameron–Martin inner product, the Hilbert–Schmidt condition,
and proves the forward support theorem via `integral_tsum` and `ae_lt_top`.

## Status

**Main result**: Fully proven

None — file is sorry-free.

**Length**: 274 lines, 7 definition(s) + 9 theorem(s)/lemma(s)

---

## Cameron-Martin inner product and norm

### `cameronMartinInner` — Definition

**Lean signature**
```lean
def cameronMartinInner (T : E →L[ℝ] H) (f g : E) : ℝ
```

**Informal**: The Cameron–Martin inner product $\langle f, g\rangle_0 = \langle Tf, Tg\rangle_H = C(f,g)$.

---

### `cameronMartinNormSq` — Definition

**Lean signature**
```lean
def cameronMartinNormSq (T : E →L[ℝ] H) (f : E) : ℝ
```

**Informal**: The Cameron–Martin norm squared $\lVert f\rVert_0^2 = \lVert Tf\rVert_H^2$.

---

### [`cameronMartinNormSq_eq_inner`](../../GaussianField/Support.lean#L63) — Theorem

**Statement**: $\lVert f\rVert_0^2 = \langle f, f\rangle_0$.

**Proof uses**: *(direct tactic proof)*

---

## Hilbert-Schmidt condition

### `IsHilbertSchmidt` — Definition

**Lean signature**
```lean
def IsHilbertSchmidt (T : E →L[ℝ] H) : Prop
```

**Informal**: $T$ is Hilbert–Schmidt w.r.t. the DM basis: $\sum_n \lVert T(e_n)\rVert^2 < \infty$.

---

### `hilbertSchmidtNormSq` — Definition

**Lean signature**
```lean
noncomputable def hilbertSchmidtNormSq (T : E →L[ℝ] H) : ℝ
```

**Informal**: The Hilbert–Schmidt norm squared $\sum_n \lVert T(e_n)\rVert^2$.

---

### `basisNormSq` — Definition

**Lean signature**
```lean
noncomputable def basisNormSq (ω : Configuration E) : ℝ
```

**Informal**: The squared basis norm of a configuration: $\sum_n \omega(e_n)^2$.

---

## Expected squared norm equals HS norm

### [`basis_second_moment`](../../GaussianField/Support.lean#L90) — Theorem

**Statement**: $\mathbb{E}[\omega(e_n)^2] = \lVert T(e_n)\rVert^2$ for each basis element $e_n$.

**Proof uses**: [`second_moment_eq_covariance`](../../GaussianField/Properties.lean#L117), `real_inner_self_eq_norm_sq`

---

### [`basis_sq_integrable`](../../GaussianField/Support.lean#L97) — Theorem

**Statement**: $\omega(e_n)^2$ is integrable under $\mu_T$ for each $n$.

**Proof uses**: [`pairing_memLp`](../../GaussianField/Properties.lean#L86), `MemLp.integrable_sq`

---

### [`basis_sq_aestronglyMeasurable`](../../GaussianField/Support.lean#L103) — Theorem

**Statement**: $\omega(e_n)^2$ is AEStronglyMeasurable under $\mu_T$.

**Proof uses**: [`basis_sq_integrable`](../../GaussianField/Support.lean#L97)

---

### [`expected_norm_sq_eq_hs`](../../GaussianField/Support.lean#L140) — Theorem

**Statement**: $\mathbb{E}\bigl[\sum_n \lvert\omega(e_n)\rvert^2\bigr] = \sum_n \lVert T(e_n)\rVert^2$ (the HS norm squared).

**Proof uses**: [`basis_sq_aestronglyMeasurable`](../../GaussianField/Support.lean#L103), [`basis_second_moment`](../../GaussianField/Support.lean#L90), `integral_tsum`, `enorm_tsum_ne_top`

---

## Forward support theorem

### [`support_of_hilbertSchmidt`](../../GaussianField/Support.lean#L159) — Theorem

**Statement**: If $T$ is Hilbert–Schmidt, then $\mu_T$-a.e. $\omega$ satisfies $\sum_n \omega(e_n)^2 < \infty$.

**Proof uses**: [`basis_sq_integrable`](../../GaussianField/Support.lean#L97), [`basis_second_moment`](../../GaussianField/Support.lean#L90), `lintegral_tsum`, `ae_lt_top`, `ENNReal.summable_toReal`, `ofReal_integral_eq_lintegral_ofReal`

---

## Weighted Hilbert-Schmidt condition and support

### `IsWeightedHS` — Definition

**Lean signature**
```lean
def IsWeightedHS (T : E →L[ℝ] H) (w : ℕ → ℝ) : Prop
```

**Informal**: Weighted Hilbert–Schmidt condition: $\sum_n w_n \lVert T(e_n)\rVert^2 < \infty$.

---

### `weightedBasisNormSq` — Definition

**Lean signature**
```lean
noncomputable def weightedBasisNormSq (w : ℕ → ℝ) (ω : Configuration E) : ℝ
```

**Informal**: Weighted basis norm: $\sum_n w_n \, \omega(e_n)^2$.

---

### [`weighted_basis_second_moment`](../../GaussianField/Support.lean#L214) — Theorem

**Statement**: $\mathbb{E}[w_n \, \omega(e_n)^2] = w_n \lVert T(e_n)\rVert^2$.

**Proof uses**: [`basis_second_moment`](../../GaussianField/Support.lean#L90), `integral_const_mul`

---

### [`weighted_basis_sq_integrable`](../../GaussianField/Support.lean#L222) — Theorem

**Statement**: $w_n \, \omega(e_n)^2$ is integrable under $\mu_T$.

**Proof uses**: [`basis_sq_integrable`](../../GaussianField/Support.lean#L97), `Integrable.const_mul`

---

### [`weighted_support`](../../GaussianField/Support.lean#L233) — Theorem

**Statement**: If $T$ is weighted-HS with nonneg weights $w$, then $\mu_T$-a.e. $\omega$ satisfies $\sum_n w_n \, \omega(e_n)^2 < \infty$.

**Proof uses**: [`weighted_basis_sq_integrable`](../../GaussianField/Support.lean#L222), [`weighted_basis_second_moment`](../../GaussianField/Support.lean#L214), `lintegral_tsum`, `ae_lt_top`, `ENNReal.summable_toReal`, `ofReal_integral_eq_lintegral_ofReal`

---

### [`isHilbertSchmidt_eq_weightedHS_one`](../../GaussianField/Support.lean#L270) — Theorem

**Statement**: `IsHilbertSchmidt T` iff `IsWeightedHS T (fun _ => 1)`.

**Proof uses**: *(direct tactic proof)*

---

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