3 Separating subalgebras

Definition 3.1

✓

A set \(\mathcal F\) of functions \(E \to F\) separates points in \(E\) if for all \(x, y \in E\) with \(x \ne y\), there exists \(f \in \mathcal F\) with \(f(x) \ne f(y)\).

Lemma 3.2

✓

In a Borel space \(E\), if two probability measures \(\mu , \nu \) on \(E\) are such that \(\mu [f] = \nu [f]\) for all \(f \in C_b(E, \mathbb {C})\), the set of bounded continuous functions from \(E\) to \(\mathbb {C}\), then \(\mu = \nu \).

Proof ▶

The Mathlib lemma MeasureTheory.FiniteMeasure.ext_of_forall_lintegral_eq shows that the result is true for \(C_b(E, \mathbb {R}_+)\). Since \(C_b(E, \mathbb {R}_{+}) \subseteq C_b(E, \mathbb {C})\), we get the result.

Lemma 3.3

✓

\(x \mapsto (t \mapsto \exp (i \langle t, x \rangle ))\) is a monoid homomorphism from \((E,+)\) to \(C_b(E, \mathbb {C})\).

Proof ▶

Lemma 3.4

✓

The functions of the form \(x \mapsto \sum _{k=1}^n a_k e^{i\langle t_k, x\rangle }\) for \(n \in \mathbb {N}\), \(a_1, \ldots , a_n \in \mathbb {R}\) and \(t_1, \ldots , t_n \in E\) are a star-subalgebra of \(C_b(E, \mathbb {C})\).

Proof ▶

The monoid homomorphism can be lifted to a homomorphism of algebras from AddMonoidAlgebra ℝ E to \(C_b(E, \mathbb {C})\) using AddMonoidAlgebra.lift. \(\mathcal M\) is the range of this homomorphism. The “star” part can be checked easily.

Let \(\mathcal M\) be the set of these functions, which we call exponential polynomials.

Lemma 3.5

The star-subalgebra \(\mathcal M\) separates points.

Proof ▶

TODO. Done in a Mathlib PR.

Lemma 3.6

✓

Let \(\mu \) be a finite measure on a Borel space \(E\) and let \(K\) be a measurable compact set such that \(\mu (K^c) \le \varepsilon \). Let \(f \in C(E, \mathbb {R})\). Then

\begin{align*} \left\vert \mu [fe^{-\varepsilon \Vert f \Vert ^2}] - \mu [f e^{-\varepsilon \Vert f \Vert ^2} \mathbb {I}_K] \right\vert \le \sqrt{\varepsilon } \: . \end{align*}

Proof ▶

Lemma 3.7

✓

For any \(f \in C_b(E, \mathbb {R})\) and a probability measure \(\mu \),

\begin{align*} \mu [f] = \lim _{\varepsilon \to 0} \mu \left[f e^{-\varepsilon \Vert f \Vert ^2} \right] \: . \end{align*}

Proof ▶

Lemma 3.8

✓

Let \(\mu , \nu \) be two finite measures in a standard Borel space \(E\). Let \(\mathcal{A}\) be a subalgebra of \(C_b(E, \mathbb {R})\) that separates points. If for all \(g \in \mathcal A\), \(\mu [g] = \nu [g]\), then for all \(f \in C_b(E, \mathbb {R})\) and all \(\varepsilon {\gt} 0\),

\begin{align*} \left\vert \mu [fe^{-\varepsilon \Vert f \Vert ^2}] - \nu [f e^{-\varepsilon \Vert f \Vert ^2}] \right\vert \le 6\sqrt{\varepsilon } \: . \end{align*}

Proof ▶

Theorem 3.9 Subalgebras separating points

✓

Let \(E\) be a complete separable pseudo-metric space. Let \(\mathcal A \subseteq C_b(E, \mathbb {C})\) be a star-subalgebra that separates points. Then if two probability measures \(\mu , \nu \) of \(E\) are such that \(\mu [f] = \nu [f]\) for all \(f \in \mathcal A\), then \(\mu = \nu \).

Proof ▶

Let \(\mu \) and \(\nu \) be two probability measures such that \(\mu [f] = \nu [f]\) for all \(f \in \mathcal A\). We want to prove that \(\mu = \nu \). By Lemma 3.2, it suffices to prove that for all \(g \in C_b(E, \mathbb {C})\), \(\mu [g] = \nu [g]\).

This is proved in Mathlib PR #19782.

Lemma 3.10

If two probability measures \(\mu , \nu \) of an inner product space \(E\) are such that \(\mu [f] = \nu [f]\) for all exponential polynomials \(f \in \mathcal M\), then \(\mu = \nu \).

Proof ▶

Apply Theorem 3.9, using Lemma 3.5.

Lemma 3.11

✓

Let \(\mathcal A\) be a subalgebra of \(C_b(E, \mathbb {C})\) that separates points. Let \(\mu , \mu _1, \mu _2, \ldots \) be probability measures, with \((\mu _n)\) tight. If for all \(f \in \mathcal A\), \(\mu _n[f] \to \mu [f]\), then \(\mu _n \xrightarrow {w} \mu \).

Proof ▶

To show convergence to \(\mu \), it suffices to show that every subsequence has a subsequence that converges to \(\mu \) (Filter.tendsto_of_subseq_tendsto). Since the family is tight, it is relatively compact by Prokhorov’s theorem. We get that each subsequence has a converging subsequence. Let then \(\mu '\) be a weak limit of \(\mu _n\). We have \(\mu _n[f] \to \mu '[f]\) and \(\mu _n[f] \to \mu [f]\) for all \(f \in \mathcal A\), hence \(\mu '[f] = \mu [f]\) for all \(f \in \mathcal A\). Since \(\mathcal A\) separates points, \(\mathcal\mu ' = \mu \) by Theorem 3.9.