blueprint work

blueprint/src/chapter/char_fun.tex

@@ -1 +1,20 @@
-\chapter{The characteristic function}
+\chapter{The characteristic function}
+
+\begin{definition}\label{def:charFun}
+Let $\mu$ be a measure on an inner product space. The characteristic function of $\mu$, denoted by $\hat{\mu}$, is the function $E \to \mathbb{C}$ defined by
+\begin{align*}
+\hat{\mu}(t) = \int_x e^{i \langle t, x \rangle} d\mu(x) \: .
+\end{align*}
+The characteristic function of a random variable $X$ is defined as the characteristic function of $\mathcal L(X)$.
+\end{definition}
+
+
+\begin{lemma}\label{lem:charFun_smul}
+\uses{def:charFun}
+For $a \in \mathbb{R}$, the characteristic function of $a X$ is $t \mapsto \phi_X(at)$.
+\end{lemma}
+
+\begin{lemma}\label{lem:charFun_add_of_indep}
+\uses{def:charFun}
+If two random variables $X, Y : \Omega \to S$ are independent, then $X+Y$ has characteristic function $\phi_{X+Y} = \phi_X \phi_Y$. 
+\end{lemma}

blueprint/src/chapter/clt.tex

@@ -1,12 +1,14 @@
 \chapter{The central limit theorem}
 
-
 \begin{theorem}[Central limit theorem]\label{clt}
-Let $\xi_1, \xi_2, \ldots$ be i.i.d. random variables with mean 0 and variance 1, and let $\zeta$ be a random variable with law $\mathcal N(0,1)$. Then
+Let $X_1, X_2, \ldots$ be i.i.d. random variables with mean 0 and variance 1, and let $Z$ be a random variable with law $\mathcal N(0,1)$. Then
 \begin{align*}
-\frac{1}{\sqrt{n}}\sum_{k=1}^n \xi_k \xrightarrow{d} \zeta \: .
+\frac{1}{\sqrt{n}}\sum_{k=1}^n X_k \xrightarrow{d} Z \: .
 \end{align*}
 \end{theorem}
 
-\begin{proof}
+\begin{proof}\uses{lem:charFun_add_of_indep}\uses{lem:charFun_smul}
+Let $S_n = \frac{1}{\sqrt{n}}\sum_{k=1}^n X_k$. Let $\phi$ be the characteristic function of $X_k$. By Lemma TODO, the characteristic function of $S_n$ is $\phi_n(t) = (\phi(n^{-1/2}t))^n$.
+
+TODO
 \end{proof}

blueprint/src/chapter/main.tex

@@ -2,6 +2,9 @@
 % Add chapters of the blueprint here.
 % This file is not meant to be built. Build src/web.tex or src/print.text instead.
 
+This document is a blueprint for the formalization of the central limit theorem in Lean.
+The main reference for the results detailed here is chapter 6 of the book Foundations of Modern Probability (3rd ed.), by Olav Kallenberg.
+
 \input{chapter/mathlib_defs}
 \input{chapter/char_fun}
 \input{chapter/clt}