Cameron–Martin theorem: $(T_h)_*\mu \ll \mu \iff h \in H_\mu$

Proved

HairerSPDE.cameron_martin

by Lucas · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-analysisgaussian-measuresprobabilityspde

Theorem 4.44 (Cameron–Martin). Let $B$ be a separable Banach space and let $\mu$ be a centred Gaussian measure on $B$ : a Borel probability measure such that the image of $\mu$ under every continuous linear functional $\ell \in B^{*}$ is a real Gaussian law, with $\int_B x\,\mu(dx)=0$ . For $h \in B$ let $T_h : B \to B$ be the translation $T_h(x) = x+h$ , and let $\|h\|_\mu$ and $H_\mu = \{h : \|h\|_\mu < \infty\}$ be the Cameron–Martin norm and space of $\mu$ . Then

(T_h)_{*}\mu \ \ll\ \mu \qquad \Longleftrightarrow \qquad h \in H_\mu .

That is, the translated measure is absolutely continuous with respect to $\mu$ precisely for the directions of finite Cameron–Martin norm; for every other direction the two measures are not merely inequivalent but mutually singular.

This is the structural theorem of infinite-dimensional Gaussian analysis. In finite dimensions every direction is admissible, because Lebesgue measure is translation invariant; the theorem says that in infinite dimensions the admissible directions form the proper subspace $H_\mu$ , which typically carries measure zero. It is the source of the Girsanov transform for Gaussian noise, of the rate function in Schilder-type large deviation principles, and of the domain of the Malliavin derivative.

Formalization Note. Gaussianity is the hypothesis that the push-forward under each continuous linear functional is a real Gaussian; centredness is the separate hypothesis $\int_B x\,\mu(dx)=0$ . The translation is $x\mapsto x+h$ and absolute continuity is the usual "null sets of $\mu$ are null sets of $(T_h)_*\mu$ ". The space $B$ is assumed complete and second countable, which is the separable Banach hypothesis of the source.

Preamble

import Mathlib
import Definitions.Def_HairerSPDE_CameronMartin

set_option autoImplicit false

open MeasureTheory ProbabilityTheory Filter
open scoped ENNReal NNReal Topology

Formal statement

namespace HairerSPDE

theorem cameron_martin {B : Type*} [NormedAddCommGroup B] [NormedSpace ℝ B] [MeasurableSpace B]
    [BorelSpace B] [CompleteSpace B] [SecondCountableTopology B]
    (μ : Measure B) [IsGaussian μ] (hμ : μ[id] = 0) (h : B) :
    μ.map (fun x ↦ x + h) ≪ μ ↔ cameronMartinNorm μ h ≠ ∞ := by sorry

end HairerSPDE

Source

M. Hairer, *An Introduction to Stochastic PDEs*, lecture notes, arXiv:0907.4178v2 (3 Jul 2023), p. 31, Theorem 4.44 (Cameron–Martin)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Provenance note: this read-back was written by the agent that drafted the Lean statements, not by an independent auditor, and should be weighed accordingly.

Throughout, $B$ is a real normed vector space that is complete and second countable (a separable Banach space), equipped with its Borel $\sigma$ -algebra, and $B^{*}$ denotes its continuous dual. For a measure $\mu$ on $B$ :

" $\mu$ is Gaussian" means: for every continuous linear functional $\ell : B \to \mathbb R$ , the push-forward of $\mu$ under $\ell$ is the real Gaussian law with mean $\int_B \ell \, d\mu$ and variance $\max(\operatorname{Var}[\ell;\mu], 0)$ ; the variance-zero case is a Dirac mass, and this property already forces $\mu$ to be a probability measure.
$C_\mu(\ell_1,\ell_2)$ denotes the covariance form: it equals $\int_B (\ell_1(x) - \int \ell_1 d\mu)(\ell_2(x) - \int \ell_2 d\mu)\, \mu(dx)$ when the identity map on $B$ is square-integrable for $\mu$ , and is defined to be $0$ otherwise.
$\|h\|_\mu$ denotes the quantity $\sup \{\, \ell(h) : \ell \in B^{*},\ C_\mu(\ell,\ell) \le 1 \,\}$ , computed in $[0,\infty]$ with each real value $\ell(h)$ first replaced by $\max(\ell(h),0)$ . The supremum ranges over all $\ell$ satisfying the constraint; $\ell = 0$ always satisfies it, so $\|h\|_\mu \ge 0$ always and $\|0\|_\mu = 0$ .

Statement. Let $\mu$ be a measure on $B$ that is Gaussian in the above sense and satisfies $\int_B x \, \mu(dx) = 0$ (the Bochner integral of the identity map vanishes). Let $h \in B$ be arbitrary. Then the following two assertions are equivalent:

the push-forward of $\mu$ under the translation $x \mapsto x + h$ is absolutely continuous with respect to $\mu$ , i.e. every $\mu$ -null Borel set is null for the translated measure;
$\|h\|_\mu \neq \infty$ , i.e. $\sup\{\ell(h) : \ell \in B^{*},\ C_\mu(\ell,\ell)\le 1\}$ is finite.

The claim is a biconditional, so both directions are asserted. The quantifier over $h$ is universal and unrestricted: $h = 0$ is included (there both sides hold, the translation being the identity), and so is the case where $\mu$ is a Dirac mass at $0$ (there $C_\mu \equiv 0$ , so the right-hand side holds only for $h = 0$ ).

Nothing stronger than absolute continuity is claimed in direction 1 — equivalence of the two measures, or an explicit density, is not part of the statement — and nothing is said about mutual singularity in the failing case.

Human review

Endorsed by Shuze Chen · Sep 13, 2026
Endorsed by Lucas · Sep 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Cameron–Martin theorem: (Th)∗μ≪μ ⟺ h∈Hμ(T_h)_*\mu \ll \mu \iff h \in H_\mu(Th​)∗​μ≪μ⟺h∈Hμ​

Cameron–Martin theorem: $(T_h)_*\mu \ll \mu \iff h \in H_\mu$