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]\).
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 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
For any \(f \in C_b(E, \mathbb {R})\) and a probability measure \(\mu \),
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\),
Let \(\mu , \nu \) be two finite measures in a standard Borel space \(E\). Let \(\mathcal{A}\) be a star-subalgebra of \(C_b(E, \mathbb {k})\) that separates points, where \(\mathbb {k}\) is \(\mathbb {R}\) or \(\mathbb {C}\). If for all \(g \in \mathcal A\), \(\mu [g] = \nu [g]\), then for all \(f \in C_b(E, \mathbb {k})\), \(\mu [f] = \nu [f]\).
Proved in Mathlib PR #19782
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 \).