Fix broken reference to Lean declarations in the blueprint

Author: YaelDillies

blueprint/src/chapter/approx_hom_pfr.tex

@@ -1,27 +1,52 @@
 \chapter{Approximate homomorphism version of PFR}
 
-\begin{definition}[Additive energy]\label{energy-def}\lean{Finset.additiveEnergy}\leanok  If $G$ is a group, and $A$ is a finite subset of $G$, the \emph{additive energy} $E(A)$ of $A$ is the number of quadruples $(a_1,a_2,a_3,a_4) \in A^4$ such that $a_1+a_2 = a_3+a_4$.
+\begin{definition}[Additive energy]
+  \label{energy-def}
+  \lean{Finset.addEnergy}
+  \leanok
+  If $G$ is a group, and $A$ is a finite subset of $G$, the \emph{additive energy} $E(A)$ of $A$
+  is the number of quadruples $(a_1,a_2,a_3,a_4) \in A^4$ such that $a_1+a_2 = a_3+a_4$.
 \end{definition}
 
-\begin{lemma}[Cauchy--Schwarz bound]\label{cs-bound}\uses{energy-def}\lean{cauchy_schwarz}\leanok  If $G$ is a group, $A,B$ are finite subsets of $G$, then
-$$ E(A) \geq \frac{|\{ (a,a') \in A \times A: a+a' \in B \}|^2}{|B|}.$$
-\end{lemma}
+\begin{lemma}[Cauchy--Schwarz bound]
+  \label{cs-bound}
+  \uses{energy-def}
+  \lean{Finset.card_sq_le_card_mul_addEnergy}
+  \leanok
 
-\begin{proof}\leanok  If $B$ is empty then the claim is trivial (with the Lean convention $0/0$), so without loss of generality $B$ is non-empty.  We can rewrite
-$$ |\{ (a,a') \in A \times A: a+a' \in B \}| = \sum_{b \in B} r(b)$$
-where $r: G \to \N$ is the counting function
-$$ r(b) := |\{ (a,a') \in A \times A: a+a' = b \}|.$$
-From double counting we have
-$$ \sum_{b \in G} r(b)^2 = E(A).$$
-The claim now follows from the Cauchy--Schwarz inequality
-$$ (\sum_{b \in B} r(b))^2 \leq |B| \sum_{b \in B} r(b)^2.$$
+  If $G$ is a group, $A,B$ are finite subsets of $G$, then
+  $$E(A) \geq \frac{|\{ (a,a') \in A \times A: a+a' \in B \}|^2}{|B|}.$$
+\end{lemma}
+\begin{proof}
+  \leanok
+
+  If $B$ is empty then the claim is trivial (with the Lean convention $0/0$),
+  so without loss of generality $B$ is non-empty.  We can rewrite
+  $$ |\{ (a,a') \in A \times A: a+a' \in B \}| = \sum_{b \in B} r(b)$$
+  where $r: G \to \N$ is the counting function
+  $$ r(b) := |\{ (a,a') \in A \times A: a+a' = b \}|.$$
+  From double counting we have
+  $$ \sum_{b \in G} r(b)^2 = E(A).$$
+  The claim now follows from the Cauchy--Schwarz inequality
+  $$ (\sum_{b \in B} r(b))^2 \leq |B| \sum_{b \in B} r(b)^2.$$
 \end{proof}
 
-\begin{lemma}[Balog--Szemer\'edi--Gowers lemma]\label{bsg}\uses{energy-def}\lean{bsg}\leanok Let $G$ be an abelian group, and let $A$ be a finite non-empty set with $E(A) \geq |A|^3 / K$ for some $K \geq 1$.  Then there is a subset $A'$ of $A$ with $|A'| \geq |A| / (C_1 K^{C_2})$ and $|A'-A'| \leq C_3 K^{C_4} |A|$, where (provisionally)
-$$ C_1 = 2^4, C_2 = 1, C_3 = 2^{10}, C_4 = 5.$$
+\begin{lemma}[Balog--Szemer\'edi--Gowers lemma]
+  \label{bsg}
+  \lean{BSG}
+  \uses{energy-def}
+  \leanok
+
+  Let $G$ be an abelian group, and let $A$ be a finite non-empty set
+  with $E(A) \geq |A|^3 / K$ for some $K \geq 1$.
+  Then there is a subset $A'$ of $A$ with $|A'| \geq |A| / (C_1 K^{C_2})$ and
+  $|A'-A'| \leq C_3 K^{C_4} |A|$, where (provisionally)
+  $$C_1 = 2^4, C_2 = 1, C_3 = 2^{10}, C_4 = 5.$$
 \end{lemma}
+\begin{proof}
+  \leanok
 
-\begin{proof}\leanok See \url{https://terrytao.files.wordpress.com/2024/01/simplebsg.pdf}
+  See \url{https://terrytao.files.wordpress.com/2024/01/simplebsg.pdf}.
 \end{proof}
 
 \begin{theorem}[Approximate homomorphism form of PFR]\label{approx-hom-pfr}\lean{approx_hom_pfr}\leanok Let $G,G'$ be finite abelian $2$-groups.

blueprint/src/chapter/distance.tex

@@ -46,14 +46,19 @@ \chapter{Entropic Ruzsa calculus}
 \begin{proof} \uses{sumset-lower-gen}\leanok This follows from \Cref{sumset-lower-gen} by conditioning to $Z = z$ and summing over $z$ (weighted by $ \bbP[Z=z]$).
 \end{proof}
 
-\begin{corollary}[Independent lower bound on sumset]\label{sumset-lower}
-  \lean{max_entropy_le_entropy_add,max_entropy_le_entropy_sub}\leanok
+\begin{corollary}[Independent lower bound on sumset]
+  \label{sumset-lower}
+  \lean{ProbabilityTheory.max_entropy_le_entropy_add, ProbabilityTheory.max_entropy_le_entropy_sub}
+  \leanok
+
   If $X,Y$ are independent $G$-valued random variables, then
-$$\max(\bbH[X], \bbH[Y]) \leq \bbH[X\pm Y].
-$$
+  $$\max(\bbH[X], \bbH[Y]) \leq \bbH[X\pm Y]. $$
 \end{corollary}
+\begin{proof}
+  \uses{sumset-lower-gen, vanish-entropy}
+  \leanok
 
-\begin{proof} \uses{sumset-lower-gen, vanish-entropy}\leanok Combine \Cref{sumset-lower-gen} with \Cref{vanish-entropy}.
+  Combine \Cref{sumset-lower-gen} with \Cref{vanish-entropy}.
 \end{proof}
 
 One random variable is said to be a copy of another if they have the same distribution.

blueprint/src/chapter/entropy.tex

@@ -28,8 +28,11 @@ \chapter{Shannon entropy inequalities}
   If $X$ is an $S$-valued random variable, then $\bbH[X] \leq \log |S|$.
 \end{lemma}
 
-\begin{proof}\uses{jensen}\leanok
-  This is a direct consequence of \Cref{jensen}.
+\begin{proof}
+  \uses{concave}
+  \leanok
+
+  This is a direct consequence of \Cref{concave} and Jensen's inequality.
 \end{proof}
 
 \begin{definition}[Uniform distribution]\label{uniform-def}\leanok
@@ -52,7 +55,12 @@ \chapter{Shannon entropy inequalities}
   If $X$ is $S$-valued random variable, then $\bbH[X] = \log |S|$ if and only if $X$ is uniformly distributed on $S$.
 \end{lemma}
 
-\begin{proof} \uses{converse-jensen}\leanok Direct computation in one direction.  Converse direction needs \Cref{converse-jensen}.
+\begin{proof}
+  \uses{concave}
+  \leanok
+
+  Direct computation in one direction.
+  Converse direction needs the strict Jensen inequality and \Cref{concave}.
 \end{proof}
 
 \begin{lemma}[Entropy of uniform random variable, II]\label{uniform-entropy-II}
@@ -181,7 +189,11 @@ \chapter{Shannon entropy inequalities}
   We have $\bbI[X:Y] \geq 0$.
 \end{lemma}
 
-\begin{proof}  \uses{jensen, alternative-mutual}\leanok An application of \Cref{jensen} and \Cref{alternative-mutual}.
+\begin{proof}
+  \uses{concave, alternative-mutual}
+  \leanok
+
+  An application of jensen's inequality and \Cref{concave, alternative-mutual}.
 \end{proof}
 
 \begin{corollary}[Subadditivity]
@@ -241,8 +253,11 @@ \chapter{Shannon entropy inequalities}
   If $X,Y$ are random variables, then $\bbI[X:Y] = 0$ if and only if $X,Y$ are independent.
   \end{lemma}
 
-  \begin{proof} \uses{converse-jensen}\leanok
-    An application of the equality case of Jensen's inequality, \Cref{converse-jensen}.
+  \begin{proof}
+    \uses{concave}
+    \leanok
+
+    An application of the equality case of Jensen's inequality and \Cref{concave}.
   \end{proof}
 
 \begin{corollary}[Additivity of entropy]\label{add-entropy}

blueprint/src/chapter/further_improvement.tex

@@ -8,7 +8,12 @@ \section{Kullback--Leibler divergence}
   $$ D_{KL}(X\Vert Y) := \sum_x \mathbf{P}(X=x) \log \frac{\mathbf{P}(X=x)}{\mathbf{P}(Y=x)}.$$
 \end{definition}
 
-\begin{lemma}[Kullback--Leibler divergence of copy]\label{kl-div-copy}\lean{KLDiv_eq_of_equiv}\leanok  If $X'$ is a copy of $X$, and $Y'$ is a copy of $Y$, then $D_{KL}(X'\Vert Y') = D_{KL}(X\Vert Y)$.
+\begin{lemma}[Kullback--Leibler divergence of copy]
+  \label{kl-div-copy}
+  \lean{ProbabilityTheory.IdentDistrib.KLDiv_eq}
+  \leanok
+
+  If $X'$ is a copy of $X$, and $Y'$ is a copy of $Y$, then $D_{KL}(X'\Vert Y') = D_{KL}(X\Vert Y)$.
 \end{lemma}
 
 \begin{proof}\uses{kl-div}\leanok  Clear from definition.

blueprint/src/chapter/jensen.tex

@@ -11,23 +11,6 @@ \chapter{Applications of Jensen's inequality}
 \end{proof}
 
 
-\begin{lemma}[Jensen]\label{jensen}
-  \lean{Real.sum_negMulLog_le} \leanok
-  If $S$ is a finite set, and $\sum_{s \in S} w_s = 1$ for some non-negative $w_s$, and $p_s \in [0,1]$ for all $s \in S$, then
-  $$ \sum_{s \in S} w_s h(p_s) \leq h(\sum_{s \in S} w_s p_s).$$
-\end{lemma}
-
-\begin{proof} \uses{concave}\leanok Apply Jensen and \Cref{concave}.
-\end{proof}
-
-\begin{lemma}[Converse Jensen]\label{converse-jensen}
-  \lean{Real.sum_negMulLog_eq_iff}\leanok
-If equality holds in the above lemma, then $p_s = \sum_{s \in S} w_s h(p_s)$ whenever $w_s \neq 0$.
-\end{lemma}
-
-\begin{proof} \uses{concave}\leanok Need some converse form of Jensen, not sure if it is already in Mathlib.  May also wish to state it as an if and only if.
-\end{proof}
-
 \begin{lemma}[log sum inequality]
   \label{log-sum}\lean{Real.sum_mul_log_div_leq}\leanok
   If $S$ is a finite set, and $a_s,b_s$ are non-negative for $s\in S$, then

blueprint/src/chapter/pfr.tex

@@ -2,7 +2,7 @@ \chapter{Proof of PFR}
 
 \begin{lemma}[Ruzsa covering lemma]
 \label{ruz-cov}
-\lean{Finset.exists_subset_mul_div}
+\lean{Finset.ruzsa_covering_mul}
 \leanok
 If $A,B$ are finite non-empty subsets of a group $G$, then $A$ can be covered by at most $|A+B|/|B|$ translates of $B-B$.
 \end{lemma}

blueprint/src/chapter/torsion.tex

@@ -278,7 +278,14 @@ \section{The tau functional}
 $$ \tau[ (X_i)_{1 \leq i \leq m}] := D[(X_i)_{1 \leq i \leq m}] + \eta \sum_{i=1}^m d[X_i; X^0].$$
 \end{definition}
 
-\begin{definition}[$\tau$-minimizer]\label{tau-min-multi}\uses{tau-def-multi}\lean{multiTau_minimizes}\leanok  A $\tau$-minimizer is a tuple $(X_i)_{1 \leq i \leq m}$ that minimizes the $\tau$-functional among all tuples of $G$-valued random variables.
+\begin{definition}[$\tau$-minimizer]
+  \label{tau-min-multi}
+  \uses{tau-def-multi}
+  \lean{multiTauMinimizes}
+  \leanok
+
+  A $\tau$-minimizer is a tuple $(X_i)_{1 \leq i \leq m}$ that minimizes the $\tau$-functional
+  among all tuples of $G$-valued random variables.
 \end{definition}
 
 \begin{proposition}[Existence of $\tau$-minimizer]\label{tau-min-exist-multi}\lean{multiTau_continuous, multiTau_min_exists}\leanok  If $G$ is finite, then a $\tau$-minimizer exists.

blueprint/src/chapter/weak_pfr.tex

@@ -162,8 +162,14 @@ \chapter{Weak PFR over the integers}
 \end{proof}
 
 
-\begin{definition}\label{dimension-def}\lean{dimension}\leanok
-If $A\subseteq \mathbb{Z}^{d}$ then by $\dim(A)$ we mean the dimension of the span of $A-A$ over the reals -- equivalently, the smallest $d'$ such that $A$ lies in a coset of a subgroup isomorphic to $\mathbb{Z}^{d'}$.
+\begin{definition}
+  \label{dimension-def}
+  \lean{AffineSpace.finrank}
+  \leanok
+
+  If $A\subseteq \mathbb{Z}^{d}$ then by $\dim(A)$ we mean the dimension of the span of $A-A$
+  over the reals -- equivalently, the smallest $d'$ such that $A$ lies in a coset of a subgroup
+  isomorphic to $\mathbb{Z}^{d'}$.
 \end{definition}
 
 
@@ -200,10 +206,15 @@ \chapter{Weak PFR over the integers}
 as required.
 \end{proof}
 
-\begin{theorem}\label{weak-pfr-symm}\lean{weak_PFR_symm}\leanok
-If $A\subseteq \mathbb{Z}^d$ is a finite non-empty set with $d[U_A;U_A]\leq \log K$ then there exists a non-empty $A'\subseteq A$ such that
-\[\lvert A'\rvert\geq K^{-17}\lvert A\rvert\]
-and $\dim A'\leq \frac{40}{\log 2} \log K$.
+\begin{theorem}
+  \label{weak-pfr-symm}
+  \lean{weak_PFR}
+  \leanok
+
+  If $A\subseteq \mathbb{Z}^d$ is a finite non-empty set with $d[U_A;U_A]\leq \log K$
+  then there exists a non-empty $A'\subseteq A$ such that
+  \[\lvert A'\rvert\geq K^{-17}\lvert A\rvert\]
+  and $\dim A'\leq \frac{40}{\log 2} \log K$.
 \end{theorem}
 \begin{proof}
 \uses{weak-pfr-asymm,dimension-def}\leanok