diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex index 891f91aa..a7c5de83 100644 --- a/blueprint/src/content.tex +++ b/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} diff --git a/blueprint/src/macros/print.tex b/blueprint/src/macros/print.tex index 668fec13..ab60ca20 100644 --- a/blueprint/src/macros/print.tex +++ b/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 \ No newline at end of file +\ExplSyntaxOff diff --git a/blueprint/src/print.tex b/blueprint/src/print.tex index 69acdf84..57211d65 100644 --- a/blueprint/src/print.tex +++ b/blueprint/src/print.tex @@ -1,22 +1,14 @@ -% 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} @@ -24,10 +16,29 @@ \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} \ No newline at end of file + +\bibliographystyle{alpha} +\bibliography{references} +\end{document} diff --git a/blueprint/src/references.bib b/blueprint/src/references.bib new file mode 100644 index 00000000..d60f7580 --- /dev/null +++ b/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} +}