# `IsGaussian.lean` -- Informal Summary

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

## Overview

Shows that the Gaussian measure constructed by this library satisfies Mathlib's `ProbabilityTheory.IsGaussian` typeclass. The key bridging argument is that every continuous linear functional $L$ on $\text{WeakDual}\,\mathbb{R}\,E$ (the weak-* topology) is evaluation at some $f \in E$: continuity in the initial topology implies $\ker L$ contains an intersection of finitely many evaluation kernels, so by linear algebra $L$ is a finite linear combination of evaluations. Once this is established, the existing `pairing_is_gaussian` immediately yields the result.

## Status

**Main result**: Fully proven

None -- file is sorry-free.

**Length**: 160 lines, 0 definition(s) + 2 theorem(s)/lemma(s)

---

### [`weakDual_clm_eq_eval`](../../GaussianField/IsGaussian.lean#L55) -- Lemma

**Statement**: Every continuous linear functional $L : (\text{WeakDual}\,\mathbb{R}\,E) \to_L \mathbb{R}$ is evaluation at some $f \in E$: there exists $f$ such that $L(\omega) = \omega(f)$ for all $\omega$.

**Proof uses**: `mem_span_of_iInf_ker_le_ker`, `Submodule.mem_span_range_iff_exists_fun`, `topDualPairing`

---

### [`measure_isGaussian`](../../GaussianField/IsGaussian.lean#L142) -- Instance

**Lean signature**
```lean
instance measure_isGaussian (T : E →L[ℝ] H) :
    ProbabilityTheory.IsGaussian (measure T)
```
**Informal**: The measure constructed from $T$ is Gaussian in the Mathlib sense: its pushforward by every continuous linear functional is a real Gaussian.

**Proof uses**: [`weakDual_clm_eq_eval`](../../GaussianField/IsGaussian.lean#L55), [`pairing_is_gaussian`](../../GaussianField/Properties.lean), [`measure_centered`](../../GaussianField/Properties.lean), [`second_moment_eq_covariance`](../../GaussianField/Properties.lean), `variance_of_integral_eq_zero`

---

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