From 299a5b3202be15d5e719b293054b04b88e22037b Mon Sep 17 00:00:00 2001
From: RemyDegenne <Remydegenne@gmail.com>
Date: Sun, 31 Dec 2023 14:20:30 +0100
Subject: [PATCH] more about Prokhorov's theorem

---
 blueprint/src/chapter/tight.tex | 17 +++++++++++++++--
 1 file changed, 15 insertions(+), 2 deletions(-)

diff --git a/blueprint/src/chapter/tight.tex b/blueprint/src/chapter/tight.tex
index ba1b8f9..da02c73 100644
--- a/blueprint/src/chapter/tight.tex
+++ b/blueprint/src/chapter/tight.tex
@@ -34,15 +34,21 @@ \chapter{Tight families of measures}
 
 \end{proof}
 
+\begin{lemma}\label{tight_closure}
+\uses{def:tight}
+The closure of a tight set of measures is tight.
+\end{lemma}
+
+\begin{proof}
+\end{proof}
 
 \section{Prokhorov's theorem}
 
 \begin{lemma}\label{lem:exists_finite_union_inter_lt}
-Let $(U_n)_{n \in \mathbb{N}}$ be measurable sets such that $\bigcap_{n=1}^{+ \infty} U_n = \emptyset$. Let $\mu$ be a measure and let $\varepsilon > 0$. Then there exists a finite set $S \subseteq \mathbb{N}$ such that $\mu(\bigcap_{n \in S} U_n) < \varepsilon$.
+Let $(U_n)_{n \in \mathbb{N}}$ be open sets in a complete separable metric space $E$ such that $\bigcup_{n=1}^{+ \infty} U_n = E$. Let $\Gamma$ be a relatively compact set of probability measures on $E$ for the topology of weak convergence of measures. Then for all $\varepsilon > 0$ there exists a finite set $S \subseteq \mathbb{N}$ such that for all $\mu \in \Gamma$, $\mu(\bigcup_{n \in S} U_n) > 1 - \varepsilon$.
 \end{lemma}
 
 \begin{proof}
-Rémy: I have a proof of that result in the project formalizing Kolmogorov's extension theorem (joint work with Peter Pfaffelhuber).
 \end{proof}
 
 \begin{lemma}\label{lem:prokhorov_aux1}
@@ -52,6 +58,13 @@ \section{Prokhorov's theorem}
 \begin{proof}\uses{lem:exists_finite_union_inter_lt}
 \end{proof}
 
+\begin{lemma}\label{ProbabilityMeasure_compact}
+If $E$ is a compact metric space, then $\mathcal P(X)$ with the Prokhorov metric is a compact metric space.
+\end{lemma}
+
+\begin{proof}
+\end{proof}
+
 \begin{theorem}[Prokhorov's theorem]\label{thm:prokhorov}
 \uses{def:tight}
 Let $E$ be a complete separable metric space and let $S \subseteq \mathcal P(E)$. Then the following are equivalent: