3 Separating subalgebras
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)\).
A set \(\mathcal F\) of functions \(E \to F\) is separating in \(\mathcal P(E)\) if for all probability measures \(\mu , \nu \) on \(E\) with \(\mu \ne \nu \), there exists \(f \in \mathcal F\) with \(\mu [f] \ne \nu [f]\).
TODO: this is a special case of a definition about duality pairings. Two types \(E\), \(F\) and a bilinear function \(B : E \times F \to \mathbb {k}\) form a pairing (in the def above \(\mathcal P(E)\), \(C_b(E, \mathbb {C})\) and the integral). A set \(\mathcal E\) of \(E\) is separating if for all \(f, f' \in F\) with \(f \ne f'\), there exists \(x \in \mathcal E\) with \(B(x, f) \ne B(x, f')\).
In a Borel space \(E\), the set \(C_b(E, \mathbb {C})\) of bounded continuous functions from \(E\) to \(\mathbb {C}\) is separating in \(\mathcal P(E)\).
The Mathlib lemma MeasureTheory.FiniteMeasure.ext_of_forall_lintegral_eq shows that \(C_b(E, \mathbb {R}_+)\) is separating. Since \(C_b(E, \mathbb {R}_{+}) \subseteq C_b(E, \mathbb {C})\), the larger set is also separating.
\(x \mapsto (t \mapsto \exp (i \langle t, x \rangle ))\) is a monoid homomorphism from \((E,+)\) to \(C_b(E, \mathbb {C})\).
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})\).
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.
The star-subalgebra \(\mathcal M\) separates points.
TODO
Let \(\mu \) be a measure on \(E\) and \(K\) be a compact set such that \(\mu (K^c) \le \varepsilon \). Let \(f \in C_b(E, \mathbb {C})\). Then
where \(C = \sup _{x \ge 0} x e^{-x^2}\).
For any \(f \in C_b(E, \mathbb {C})\) and probability measures \(\mu , \nu \),
For \(f \in \mathcal A\) a subalgebra of \(C_b(E, \mathbb {C})\), \(\varepsilon \ge 0\) and \(n \in \mathbb {N}\), \(f (1 - \frac{\varepsilon }{n} f)^n \in \mathcal A\). Furthermore, for a measure \(\mu \),
Dominated convergence.
Let \(\mathcal A\) be a subalgebra of \(C_b(E, \mathbb {C})\) that separates points. Let \(\mu , \nu \) be two probability measures. If for all \(f \in \mathcal A\), \(\mu [f] = \nu [f]\), then for all \(g \in C_b(E, \mathbb {C})\), \(\mu [g] = \nu [g]\).
Let \(g \in C_b(E, \mathbb {C})\) and \(\varepsilon {\gt} 0\).
By Lemma 3.8, it suffices to show that \(\lim _{\varepsilon \to 0} \left\vert \mu \left[g e^{-\varepsilon \Vert g \Vert ^2} \right] - \nu \left[g e^{-\varepsilon \Vert g \Vert ^2} \right] \right\vert = 0\).
The two measures are inner regular, hence there exists \(K\) compact with \(\mu (K^c) \le \varepsilon \) and \(\nu (K^c) \le \varepsilon \).
By Lemma 3.7, it suffices to show that \(\lim _{\varepsilon \to 0} \left\vert \mu \left[g e^{-\varepsilon \Vert g \Vert ^2} \mathbb {I}_K \right] - \nu \left[g e^{-\varepsilon \Vert g \Vert ^2} \mathbb {I}_K \right] \right\vert = 0\).
On \(K\), the Stone-Weierstrass theorem ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints gives that a subalgebra that separates points is dense. There exists then \(f \in \mathcal A\) such that \(\sup _{x \in K} \left\vert f(x) - g(x) \right\vert \le \varepsilon \).
TODO: we can bound \(\left\vert \mu \left[g e^{-\varepsilon \Vert g \Vert ^2} \mathbb {I}_K \right] - \mu \left[f e^{-\varepsilon \Vert f \Vert ^2} \mathbb {I}_K \right] \right\vert \) by a function of \(\varepsilon \) tending to 0. Same for \(\nu \).
It remains to show that \(\lim _{\varepsilon \to 0} \left\vert \mu \left[f e^{-\varepsilon \Vert f \Vert ^2} \mathbb {I}_K \right] - \nu \left[f e^{-\varepsilon \Vert f \Vert ^2} \mathbb {I}_K \right] \right\vert = 0\).
TODO. Use 3.9 to use that \(\mu [f'] = \nu [f']\) for all \(f' \in \mathcal A\).
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 \(\mathcal A\) is separating in \(\mathcal P(E)\).
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 \). Since \(C_b(E, \mathbb {C})\) is separating, it suffices to prove that for \(g \in C_b(E, \mathbb {C})\), \(\mu [g] = \nu [g]\). This is proved in Lemma 3.10
The exponential polynomials \(\mathcal M\) are separating.
Let \(\mathcal A\) be a separating subalgebra of \(C_b(E, \mathbb {C})\). 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 \).
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\) is separating, \(\mathcal\mu ' = \mu \).
Alternative proof without Prokhorov’s theorem: we can proceed similarly to the proof of Lemma 3.10, starting with: let \(K\) be a compact such that \(\mu (K^c) \le \varepsilon \) and \(\mu _n(K^c) \le \varepsilon \) for all \(n\), which exists since the family is tight. Etc. (check that this works)