refactor M separating

blueprint/src/chapter/char_fun.tex

@@ -126,24 +126,29 @@ \subsection{Characteristic function and tightness}
 
 Remark: the finite dimension is necessary. Counterexample: $\ell^2$ with $\mu_n$ the law of $X_n = \sum_{k=1}^n \zeta_k e_k$ where $e_k = (0, \ldots, 0, 1, 0 \ldots)$ and the $\zeta_k$ are i.i.d. $\mathcal N(0,1)$. Then $\hat{\mu}_n(t) \to e^{- \Vert t \Vert^2 / 2}$ for all $t \in \ell^2$ but $(\mu_n)$ is not tight (todo: why?).
 
+\begin{lemma}\label{lem:eq_M_of_eq_charFun}
+If two probability measures $\mu, \nu$ have same characteristic function, then for all exponential polynomial $f \in \mathcal M$, $\mu[f] = \nu[f]$.
+\end{lemma}
+
+\begin{proof}\uses{lem:starSubalgebra_expPoly}
+\end{proof}
+
 \begin{lemma}\label{lem:ext_charFun}
 Two probability measures on a TODO space are equal iff they have the same characteristic function.
 \end{lemma}
 
-\begin{proof}\uses{lem:separating_expPoly, thm:separating_starSubalgebra}
-The sub-algebra $\mathcal M$ of exponential polynomials is separating by Lemma~\ref{lem:separating_expPoly} and Theorem~\ref{thm:separating_starSubalgebra}. Equality of characteristic functions implies equality on $\mathcal M$, which then implies equality of the measures since $\mathcal M$ is separating.
+\begin{proof}\uses{lem:separating_expPoly, lem:eq_M_of_eq_charFun}
+The sub-algebra $\mathcal M$ of exponential polynomials is separating by Lemma~\ref{separating_expPoly}. Equality of characteristic functions implies equality on $\mathcal M$ by Lemma~\ref{lem:eq_M_of_eq_charFun}, which then implies equality of the measures since $\mathcal M$ is separating.
 \end{proof}
 
 \begin{theorem}[Convergence of characteristic functions and weak convergence of measures]\label{thm:charFun_tendsto_iff_measure_tendsto}
 Let $\mu, \mu_1, \mu_2, \ldots$ be probability measures on $\mathbb{R}^d$ with characteristic functions $\hat{\mu}, \hat{\mu}_1, \hat{\mu}_2, \ldots$. Then $\mu_n \xrightarrow{w} \mu$ iff for all $t$, $\hat{\mu}_n(t) \to \hat{\mu}(t)$.
 \end{theorem}
 
-\begin{proof}\uses{lem:separating_expPoly, lem:tight_of_tendsto_charFun, lem:cvg_of_separating}
+\begin{proof}\uses{lem:separating_expPoly, lem:tight_of_tendsto_charFun, lem:cvg_of_separating, lem:eq_M_of_eq_charFun}
 For all $t$, $x \mapsto e^{i \langle t, x \rangle}$ is a bounded continuous function. Hence by the definition of convergence in distribution, $\mu_n \xrightarrow{w} \mu \implies \hat{\mu}_n(t) \to \hat{\mu}(t)$ for all $t$.
 
 Let's now prove the other direction.
 If the characteristic functions converge pointwise, we get from Lemma~\ref{lem:tight_of_tendsto_charFun} that the family of measures is tight. 
-Then apply Lemma~\ref{lem:cvg_of_separating} to the subalbegra $\mathcal M$: it suffices to show that $\mu_n[f] \to \mu[f]$ for all $f \in \mathcal M$.
-
-TODO
+Then apply Lemma~\ref{lem:cvg_of_separating} to the subalbegra $\mathcal M$: it suffices to show that $\mu_n[f] \to \mu[f]$ for all $f \in \mathcal M$. This is obtained with Lemma~\ref{lem:eq_M_of_eq_charFun}.
 \end{proof}

blueprint/src/chapter/separating.tex

@@ -39,7 +39,7 @@ \chapter{Separating subalgebras}
 
 Let $\mathcal M$ be the set of these functions, which we call exponential polynomials.
 
-\begin{lemma}\label{lem:separating_expPoly}
+\begin{lemma}\label{lem:separates_points_expPoly}
 \lean{Clt.expPoly_separatesPoints} \leanok
 \uses{lem:starSubalgebra_expPoly}
 The star-subalgebra $\mathcal M$ separates points.
@@ -123,6 +123,14 @@ \chapter{Separating subalgebras}
 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~\ref{lem:Cb_eq_of_separating}
 \end{proof}
 
+\begin{lemma}\label{lem:separating_expPoly}
+The exponential polynomials $\mathcal M$ are separating.
+\end{lemma}
+
+\begin{proof}\uses{thm:separating_starSubalgebra, lem:separates_points_expPoly}
+Apply Theorem~\ref{thm:separating_starSubalgebra}, using Lemma~\ref{lem:separates_points_expPoly}.
+\end{proof}
+
 \begin{lemma}\label{lem:cvg_of_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$.
 \end{lemma}