docs(blueprint): article-class restructure, narrative, examples, conclusion

blueprint/src/content.tex

@@ -3,8 +3,12 @@
 
 \chapter{Introduction}
 
-This blueprint documents the formalization of \textbf{de Finetti's theorem} and the
+This document presents the mathematical blueprint for a Lean~4 formalization of
+\textbf{de Finetti's theorem} and the
 \textbf{de Finetti--Ryll-Nardzewski equivalence} for infinite sequences on \emph{standard Borel spaces}.
+It maps each definition and theorem in the formalization to its mathematical counterpart,
+records the proof-level dependency structure, and links to the corresponding Lean declarations.
+The companion web version of this blueprint renders an interactive dependency graph.
 
 The main result establishes a three-way equivalence between:
 \begin{itemize}
@@ -13,13 +17,54 @@ \chapter{Introduction}
   \item \textbf{Conditionally i.i.d.}: There exists a probability kernel such that finite marginals equal mixtures of product measures
 \end{itemize}
 
-We formalize \emph{all three proofs} from Kallenberg (2005):
+We formalize \emph{all three proofs} from Kallenberg~\cite{Kallenberg2005}:
 \begin{enumerate}
   \item \textbf{Koopman/Ergodic approach} using the Mean Ergodic Theorem
   \item \textbf{L$^2$ approach} using elementary contractability bounds
-  \item \textbf{Martingale approach} using reverse martingale convergence (after Aldous)
+  \item \textbf{Martingale approach} using reverse martingale convergence (after Aldous~\cite{Aldous1985})
 \end{enumerate}
 
+\begin{table}[h]
+\centering
+\small
+\begin{tabular}{@{}llll@{}}
+\toprule
+\textbf{Route} & \textbf{Key tool} & \textbf{Extra assumptions} & \textbf{Lines} \\
+\midrule
+Martingale & Reverse martingale convergence & None (general $\alpha$) & 3,770 \\
+L$^2$ & Ces\`aro $L^2$ bounds & $\alpha = \mathbb{R}$, square-integrable & 12,476 \\
+Koopman & Mean Ergodic Theorem & None (general $\alpha$) & 6,893 \\
+\bottomrule
+\end{tabular}
+\end{table}
+
+\paragraph{Contributions.}
+The formalization comprises approximately 43,500 lines of Lean~4 across 112 files.
+All three proof routes share a uniform ``common ending'' that packages conditional factorization
+into a measurable directing kernel, avoiding duplication of measurability and product-measure
+uniqueness arguments.
+
+\paragraph{Setting and conventions.}
+Throughout, we fix a probability space $(\Omega, \mathcal{F}, \mu)$ and a sequence
+$X : \mathbb{N} \to \Omega \to \alpha$ of random variables taking values in
+a standard Borel space~$\alpha$ (assumed nonempty).
+Conditional expectations are with respect to~$\mu$;
+$L^2$ denotes $L^2(\Omega, \mu)$.
+Measurability is always with respect to the Borel $\sigma$-algebra on~$\alpha$
+and the ambient $\sigma$-algebra~$\mathcal{F}$ on~$\Omega$.
+
+\paragraph{Terminology.}
+Kallenberg~\cite{Kallenberg2005} uses \emph{contractable} for the subsequence-invariance property
+that some authors call \emph{spreadable} or \emph{subsymmetric}.
+We follow Kallenberg's terminology throughout.
+
+The remainder of this document is organized as follows:
+Foundations (core definitions, $\sigma$-algebra infrastructure),
+Elementary Implications (the two easy directions),
+Main Implication (three independent proofs of contractable $\Rightarrow$ conditionally i.i.d.),
+Shared Final Step (the common ending), and
+the de Finetti--Ryll-Nardzewski Equivalence (assembling the full result).
+
 
 \chapter{Foundations}
 
@@ -56,6 +101,12 @@ \section{Core Definitions}
   of $(X_{k(0)}, \ldots, X_{k(m-1)})$ equals the mixture $\mu.\mathrm{bind}(\omega \mapsto \nu(\omega)^{\otimes m})$.
 \end{definition}
 
+\paragraph{Example (Polya urn / Beta-Bernoulli).}
+Draw $p \sim \mathrm{Uniform}[0,1]$, then $X_i \mid p \sim \mathrm{Bernoulli}(p)$ independently.
+The sequence $(X_i)$ is exchangeable (by symmetry of the product) and conditionally i.i.d.\
+with directing measure $\nu(\omega) = \mathrm{Bernoulli}(p(\omega))$.
+De Finetti's theorem says every exchangeable $\{0,1\}$-valued sequence arises in this way.
+
 \section{\texorpdfstring{$\sigma$}{σ}-algebra Infrastructure}
 
 \begin{definition}[Tail $\sigma$-algebra]
@@ -106,7 +157,12 @@ \section{\texorpdfstring{$\sigma$}{σ}-algebra Infrastructure}
 \end{definition}
 
 
-\chapter{Easy Directions}
+\chapter{Elementary Implications}
+
+Two of the three implications are straightforward.
+Exchangeability implies contractability via a permutation extension argument,
+and the converse direction (conditionally i.i.d.\ implies exchangeable) follows from
+the symmetry of product measures.
 
 \section{Exchangeable implies Contractable}
 
@@ -139,12 +195,24 @@ \section{Conditionally i.i.d.\ implies Exchangeable}
 
 \chapter{Main Implication: Contractable implies Conditionally i.i.d.}
 
-This is the deep direction of de Finetti's theorem. We formalize three independent proofs.
+This is the deep direction of de Finetti's theorem.
+Each proof route extracts a conditional factorization from the symmetry hypothesis, but uses
+different analytical tools: reverse martingale convergence, $L^2$ bounds, or the mean ergodic theorem.
+All three routes ultimately feed the shared final step described in the next chapter.
 
 \section{Via Martingale (Aldous' proof)}
 
 The martingale approach uses reverse martingale convergence to the tail $\sigma$-algebra.
 
+\paragraph{Key idea.}
+Contractability implies that conditional expectations of indicators
+$\mathbb{E}[\mathbf{1}_{X_k \in B} \mid \mathcal{F}_m]$ are independent of the index~$k$
+for $k \le m$.
+These form a reverse martingale with respect to the future filtration~$(\mathcal{F}_m)$.
+The reverse martingale convergence theorem yields $L^1$ convergence to
+$\mathbb{E}[\mathbf{1}_{X_0 \in B} \mid \mathcal{T}]$, from which the directing measure and
+conditional factorization are extracted.
+
 \subsection{Pair Law Equality}
 
 \begin{lemma}[Pair law equality for contractable sequences]
@@ -267,6 +335,14 @@ \section{\texorpdfstring{Via L$^2$}{Via L²} (Elementary proof)}
 \textbf{Note:} This proof applies to \emph{real-valued} sequences ($X : \mathbb{N} \to \Omega \to \mathbb{R}$)
 with $L^2$ integrability (i.e., $\mathbb{E}[X_i^2] < \infty$ for all $i$).
 
+\paragraph{Key idea.}
+Contractability forces the covariance $\mathrm{Cov}(f(X_i), f(X_j))$ to be constant
+for $i \ne j$, which gives $L^2$ bounds on block-average differences.
+Ces\`aro averaging and these bounds yield $L^2$ (hence $L^1$) convergence of
+empirical averages $\frac{1}{n}\sum f(X_i)$ to a limiting function.
+This limit, evaluated on indicator functions $f = \mathbf{1}_{(-\infty, t]}$, produces a CDF
+from which a Stieltjes probability measure (the directing measure) is constructed.
+
 \subsection{Block Averages and Covariance Structure}
 
 \begin{definition}[Block average (L$^2$ version)]
@@ -373,6 +449,14 @@ \section{Via Koopman (Mean Ergodic Theorem)}
 The Koopman approach uses the Mean Ergodic Theorem via the shift operator on L$^2$.
 This is Kallenberg's ``first proof'' and uses disjoint-block averaging.
 
+\paragraph{Key idea.}
+The shift map $\theta$ on path space $\alpha^{\mathbb{N}}$ induces a Koopman operator on $L^2$.
+For a shift-invariant measure, the mean ergodic theorem gives $L^2$ convergence of
+Birkhoff averages to the orthogonal projection onto the shift-invariant subspace, i.e.,
+the conditional expectation given the shift-invariant $\sigma$-algebra~$\mathcal{I}$.
+Contractability then implies that products of conditional expectations factor,
+yielding the conditional independence needed for the common ending.
+
 \subsection{Block Averages and Ergodic Theory}
 
 \begin{definition}[Block average]
@@ -467,10 +551,12 @@ \subsection{Contractability and Factorization}
 \end{theorem}
 
 
-\chapter{Common Ending}
+\chapter{Shared Final Step}
 
-All three proofs converge to the same final step: extending from indicators to general sets
-via a monotone class argument.
+All three proofs converge to the same final step.
+Given conditional factorization on indicators (produced by any of the three routes above),
+the common ending extends it to full measurable sets via a $\pi$-system/monotone class argument
+and packages the result as a measurable directing kernel.
 
 \begin{lemma}[$\pi$-system uniqueness]
   \label{lem:pi_system}
@@ -496,7 +582,7 @@ \chapter{Common Ending}
 \end{theorem}
 
 
-\chapter{Main Theorem}
+\chapter{The de Finetti--Ryll-Nardzewski Equivalence}
 
 \begin{theorem}[de Finetti--Ryll-Nardzewski equivalence]
   \label{thm:deFinetti}
@@ -513,3 +599,24 @@ \chapter{Main Theorem}
   \textbf{Remark:} The martingale proof constructs $\nu$ from the tail $\sigma$-algebra $\mathcal{T}$
   via $\nu(\omega)(B) = \mathbb{E}[\mathbf{1}_{X_0 \in B} \mid \mathcal{T}](\omega)$.
 \end{theorem}
+
+
+\chapter{Conclusion and Future Work}
+
+The formalization is complete: all three proof routes compile, share a common ending, and
+assemble into the full de Finetti--Ryll-Nardzewski equivalence.
+The Lean kernel verifies that only standard axioms are used.
+
+Several directions remain for future work:
+\begin{itemize}
+  \item \textbf{Upstreaming to mathlib.}
+    Reusable components---exchangeability and contractability definitions,
+    finite-marginal reindexing lemmas, conditional independence infrastructure---are
+    candidates for staged contribution to mathlib~\cite{mathlib}.
+  \item \textbf{Partial exchangeability.}
+    Extending the formalization to Aldous--Hoover-type results for
+    partially exchangeable arrays.
+  \item \textbf{Parametric families.}
+    Connecting the directing measure to exponential family theory
+    and Bayesian nonparametrics (e.g., Dirichlet process mixtures).
+\end{itemize}

blueprint/src/macros/print.tex

@@ -1,14 +1,25 @@
-% In this file you should put macros to be used only by
+% In this file you should put macros to be used only by
 % the printed version. Of course they should have a corresponding
 % version in macros/web.tex.
 % Typically the printed version could have more fancy decorations.
-% This should be a very short file.
 %
 % This file starts with dummy macros that ensure the pdf
 % compiler will ignore macros provided by plasTeX that make
 % sense only for the web version, such as dependency graph
 % macros.
 
+% --- Chapter-to-section remapping (print only) ---
+% content.tex uses \chapter for web navigation; in the article-class
+% print PDF we remap to sections for a compact layout.
+% The article class has no \chapter, so we define it as \section.
+% We save the original \section and \subsection first, then remap.
+\makeatletter
+\let\print@origsection\section
+\let\print@origsubsection\subsection
+\newcommand{\chapter}[1]{\print@origsection{#1}}
+\renewcommand{\section}[1]{\print@origsubsection{#1}}
+\renewcommand{\subsection}[1]{\subsubsection{#1}}
+\makeatother
 
 % Dummy macros that make sense only for web version.
 \newcommand{\lean}[1]{}
@@ -26,4 +37,4 @@
 \NewDocumentCommand{\proves}{m}
  {\clist_map_inline:nn{#1}{\vphantom{\ref{##1}}}%
   \ignorespaces}
-\ExplSyntaxOff
+\ExplSyntaxOff

blueprint/src/print.tex

@@ -1,33 +1,44 @@
-% This file makes a printable version of the blueprint
-% It should include all the \usepackage needed for the pdf version.
-% The template version assume you want to use a modern TeX compiler
-% such as xeLaTeX or luaLaTeX including support for unicode
-% and Latin Modern Math font with standard bugfixes applied.
-% It also uses expl3 in order to support macros related to the dependency graph.
-% It also includes standard AMS packages (and their improved version
-% mathtools) as well as support for links with a sober decoration
-% (no ugly rectangles around links).
-% It is otherwise a very minimal preamble (you should probably at least
-% add cleveref and tikz-cd).
-
-\documentclass[letter]{report}
-
-\usepackage{geometry}
+% This file makes a printable version of the blueprint.
+% It uses XeLaTeX with unicode-math and article class for a compact layout.
+
+\documentclass[letter]{article}
+
+\usepackage[margin=1in]{geometry}
 
 \usepackage{expl3}
 
 \usepackage{amssymb, amsthm, mathtools}
+\usepackage{booktabs}
 \usepackage[unicode,colorlinks=true,linkcolor=blue,urlcolor=magenta, citecolor=blue]{hyperref}
 
 \usepackage[warnings-off={mathtools-colon,mathtools-overbracket}]{unicode-math}
 
 \input{macros/common}
 \input{macros/print}
 
-\title{Exchangeability and de Finetti's theorem}
+\title{Exchangeability and de Finetti's Theorem:\\A Lean 4 Formalization Blueprint}
 \author{Cameron Freer}
+\date{}
 
 \begin{document}
+
 \maketitle
+
+\begin{abstract}
+This document provides the mathematical blueprint for a Lean~4 formalization of
+the de Finetti--Ryll-Nardzewski theorem on standard Borel spaces.
+We describe the definitions, lemmas, and proof structure underlying three
+independent proofs of the core implication---via reverse martingales,
+$L^2$ bounds, and the mean ergodic theorem---all sharing a uniform common ending.
+The formalization comprises approximately 43,500 lines of Lean across 112 files.
+\end{abstract}
+
+{\small\tableofcontents}
+
+\bigskip
+
 \input{content}
-\end{document}
+
+\bibliographystyle{alpha}
+\bibliography{references}
+\end{document}

blueprint/src/references.bib

@@ -0,0 +1,67 @@
+@article{deFinetti1931,
+  author  = {Bruno de Finetti},
+  title   = {Funzione caratteristica di un fenomeno aleatorio},
+  journal = {Atti della R.\ Accademia Nazionale dei Lincei, Memorie, Classe di Scienze Fisiche, Matematiche e Naturali},
+  volume  = {4},
+  pages   = {251--299},
+  year    = {1931}
+}
+
+@article{RyllNardzewski1957,
+  author  = {Czes{\l}aw Ryll-Nardzewski},
+  title   = {On stationary sequences of random variables and the de Finetti's equivalence},
+  journal = {Colloquium Mathematicum},
+  volume  = {4},
+  number  = {2},
+  pages   = {149--156},
+  year    = {1957},
+  doi     = {10.4064/cm-4-2-149-156}
+}
+
+@book{Kallenberg2005,
+  author    = {Olav Kallenberg},
+  title     = {Probabilistic Symmetries and Invariance Principles},
+  series    = {Probability and Its Applications},
+  publisher = {Springer},
+  year      = {2005},
+  doi       = {10.1007/0-387-28861-9}
+}
+
+@incollection{Aldous1985,
+  author    = {David J. Aldous},
+  title     = {Exchangeability and related topics},
+  booktitle = {Ecole d'Ete de Probabilites de Saint-Flour XIII --- 1983},
+  series    = {Lecture Notes in Mathematics},
+  volume    = {1117},
+  pages     = {1--198},
+  publisher = {Springer},
+  year      = {1985},
+  doi       = {10.1007/BFb0099421}
+}
+
+@article{HewittSavage1955,
+  author  = {Edwin Hewitt and Leonard J. Savage},
+  title   = {Symmetric measures on {C}artesian products},
+  journal = {Transactions of the American Mathematical Society},
+  volume  = {80},
+  number  = {2},
+  pages   = {470--501},
+  year    = {1955},
+  doi     = {10.1090/S0002-9947-1955-0076206-8}
+}
+
+@misc{mathlib,
+  author       = {{mathlib community}},
+  title        = {mathlib4: {T}he math library of {L}ean 4},
+  howpublished = {GitHub repository},
+  year         = {2024},
+  url          = {https://github.com/leanprover-community/mathlib4}
+}
+
+@misc{leanblueprint,
+  author       = {Patrick Massot},
+  title        = {leanblueprint: {A} tool for {L}ean formalization blueprints},
+  howpublished = {GitHub repository},
+  year         = {2024},
+  url          = {https://github.com/PatrickMassot/leanblueprint}
+}