minor blueprint work

blueprint/src/chapter/char_fun.tex

@@ -0,0 +1 @@
+\chapter{The characteristic function}

blueprint/src/chapter/clt.tex

@@ -32,3 +32,6 @@ \chapter{The central limit theorem}
 \frac{1}{\sqrt{n}}\sum_{k=1}^n \xi_k \xrightarrow{d} \zeta \: .
 \end{align*}
 \end{theorem}
+
+\begin{proof}
+\end{proof}

blueprint/src/chapter/main.tex

@@ -2,5 +2,6 @@
 % Add chapters of the blueprint here.
 % This file is not meant to be built. Build src/web.tex or src/print.text instead.
 
+\input{chapter/mathlib_defs}
 \input{chapter/char_fun}
 \input{chapter/clt}

blueprint/src/chapter/mathlib_defs.tex

@@ -0,0 +1,10 @@
+\chapter{Useful definitions from Mathlib}
+
+\begin{definition}[Convergence in probability]\label{def:cvg_probability}
+\lean{MeasureTheory.TendstoInMeasure} \leanok
+We say that $(\xi_i)_{i \in \mathbb{N}}$ tends to $\xi$ in probability (or in measure) if for all $\varepsilon > 0$
+\begin{align*}
+\mathbb{P}(d(\xi_n, \xi) \ge \varepsilon) \to_{n \to +\infty} 0
+\end{align*}
+
+\end{definition}