Gettting blueprint to compile

PFR/entropy_pfr.lean

@@ -0,0 +1,17 @@
+import PFR.f2_vec
+import PFR.ruzsa_distance
+
+/-!
+# Entropic version of polynomial Freiman-Ruzsa conjecture
+
+Here we prove the entropic version of the polynomial Freiman-Ruzsa conjecture.
+
+## Main results
+
+* `entropic_PFR_conjecture`: For two $G$-valued random variables $X^0_1, X^0_2$, there is some subgroup $H \leq G$ such that $d[X^0_1;U_H] + d[X^0_2;U_H] \le 11 d[X^0_1;X^0_2]$.
+
+-/
+
+
+/-- `entropic_PFR_conjecture`: For two $G$-valued random variables $X^0_1, X^0_2$, there is some subgroup $H \leq G$ such that $d[X^0_1;U_H] + d[X^0_2;U_H] \le 11 d[X^0_1;X^0_2]$. -/
+theorem entropic_PFR_conjecture : 0 = 1 := by sorry

PFR/main.lean

@@ -3,6 +3,7 @@ import Mathlib.Data.Real.Basic
 import Mathlib.GroupTheory.OrderOfElement
 import PFR.f2_vec
 import PFR.ruzsa_covering
+import PFR.entropy_pfr
 
 /-!
 # Polynomial Freiman-Ruzsa conjecture

PFR/ruzsa_distance.lean

@@ -25,6 +25,9 @@ variable {Ω Ω' Ω'' G : Type*} [mΩ : MeasurableSpace Ω] {μ : Measure Ω} [m
 /-- The Ruzsa distance `dist X Y` between two random variables is defined as $H[X'-Y'] - H[X']/2 - H[Y']/2$, where $X',Y'$ are independent copies of $X, Y$. -/
 def dist (X : Ω → G) (Y : Ω' → G) : ℝ := sorry
 
+-- may also want to make further notations for Ruzsa distance
+
+
 /-- The Ruzsa triangle inequality -/
 lemma Ruzsa_triangle (X : Ω → G) (Y : Ω' → G) (Z : Ω'' → G) : dist X Z ≤ dist X Y + dist Y Z := sorry
 

blueprint/src/chapter/distance.tex

@@ -45,7 +45,7 @@ \chapter{Ruzsa calculus}
 \begin{lemma}[Copy preserves entropy]\label{copy-ent}\uses{copy-def,entropy-def} If $X'$ is a copy of $X$ then $H[X'] = H[X]$.
 \end{lemma}
 
-\begin{proof} Immediate from Definitions \ref{copy-def, entropy-def}.
+\begin{proof} Immediate from Definitions \ref{copy-def}, \ref{entropy-def}.
 \end{proof}
 
 \begin{lemma}[Existence of independent copies]\label{independent-exist} \uses{copy-def, independent-def} Let $X_i : \Omega_i \to S_i$ be random variables for $i=1,\dots,k$.  Then there exist jointly independent random variables $X'_i: \Omega' \to S_i$ for $i=1,\dots,k$ such that each $X'_i$ is a copy of $X_i$.
@@ -106,7 +106,7 @@ \chapter{Ruzsa calculus}
 $$ d[X;Y] \leq d[X;Z] + d[Z;Y].$$
 \end{lemma}
 
-\begin{proof}\uses{conditional-nonneg,subadditive, relabeled-entropy, additive, ruz-indep} By Lemma \ref{ruz-copy} and Lemmas \ref{independent-exist, ruz-indep}, it suffices to show that
+\begin{proof}\uses{conditional-nonneg,subadditive, relabeled-entropy, additive, ruz-indep} By Lemma \ref{ruz-copy} and Lemmas \ref{independent-exist}, \ref{ruz-indep}, it suffices to show that
 \begin{equation}\label{submod-explicit} H[X - Y] \leq H[X-Z] + H[Z-Y] - H[Z]\end{equation}
 whenever $X, Y, Z$ are independent. To prove this, apply Corollary \ref{alt-submodularity} to obtain
 \[ H[X - Z, X - Y] + H[Y, X - Y] \geq H[X - Z, Y, X - Y] + H[X - Y].\]
@@ -138,7 +138,7 @@ \chapter{Ruzsa calculus}
 \begin{proof}\uses{submodularity, additive, relabeled-entropy}
 From Lemma \ref{submodularity} we have
 $$ H[X, X+Y+Z] + H[Z, X+Y+Z] \geq H[X, Z, X+Y+Z] + H[X+Y+Z].$$
-However, using Lemmas \ref{additive}, \ref{relabeled-entropy} repeatedly we have $H[X, X+Y+Z] = H[X, Y+Z] = H[X] + H[Y+Z]$, $H[Z, X+Y + Z] = H[Z, X+Y] = H[Z] + H[X+Y]$ and $H[X, Z, X+Y+Z] = H[X, Y, Z] = H[X] + H[Y] + H[Z]$.  The claim then follows from a calculation.
+However, using Lemmas \ref{add-entropy}, \ref{relabeled-entropy} repeatedly we have $H[X, X+Y+Z] = H[X, Y+Z] = H[X] + H[Y+Z]$, $H[Z, X+Y + Z] = H[Z, X+Y] = H[Z] + H[X+Y]$ and $H[X, Z, X+Y+Z] = H[X, Y, Z] = H[X] + H[Y] + H[Z]$.  The claim then follows from a calculation.
 \end{proof}
 
 \begin{definition}[Conditionally independent trials]\label{cond-trial}  Let $X,Y$ be random variables on a space $\Omega$.
@@ -194,7 +194,7 @@ \chapter{Ruzsa calculus}
 Finally, we have
 \begin{equation}\label{bsg-25} H[A_1 - B_2, B_1] = H[A_2 - B_1, B_1] = H[A_2, B_1] \leq H[A] + H[B].\end{equation}
 Substituting~\eqref{bsg-24},~\eqref{bsg-23} and~\eqref{bsg-25} into~\eqref{bsg-31} yields
-\[ H[A_1 - B_2] \leq 2I[A:B] + H[Z]\] and so by~\eqref{cond-dec}
+\[ H[A_1 - B_2] \leq 2I[A:B] + H[Z]\] and so by Corollary \ref{cond-reduce}
 \[H[A_1 - B_2 | Z]  \leq 2I[A:B] + H[Z].\]
 Since
 \begin{align*} H[A_1 | Z] & = H[A_1, A_1 + B_1] - H[Z] \\ & = H[A,B] - H[Z] \\ & = H[Z] - I[A:B] - 2 H[Z]-H[A]-\bbH[B]\end{align*}

blueprint/src/chapter/pfr.tex

@@ -9,10 +9,10 @@ \chapter{Proof of PFR}
 \begin{theorem}[PFR]\label{pfr}  If $A \subset {\bf F}_2^n$ and $|A+A| \leq K|A|$, then $A$ can be covered by most $2K^{12}$ translates of a subspace $H$ of ${\bf F}_2^n$ with $|H| \leq |A|$.
 \end{theorem}
 
-\begin{proof}\uses{pfr-entropy, uniform-entropy, jensen-bound,ruz-dist-def,ruzsa-diff,bound-conc,ruz-cov}
+\begin{proof}\uses{entropy-pfr, uniform-entropy, jensen-bound,ruz-dist-def,ruzsa-diff,bound-conc,ruz-cov}
   Let $U_A$ be the uniform distribution on $A$, thus $H[U_A] = \log |A|$ by Lemma \ref{uniform-entropy}. By Lemma \ref{jensen-bound} and the fact that $U_A + U_A$ is supported on $A + A$, $H[U_A + U_A] \leq \log|A+A|$. By Definition \ref{ruz-dist-def}, the doubling condition $|A+A| \leq K|A|$ therefore gives
   \[ d[U_A;U_A] \leq \log K.\]
-  By Theorem \ref{pfr-entropy}, we may thus find a subspace $H$ of $\F_2^n$ such that
+  By Theorem \ref{entropy-pfr}, we may thus find a subspace $H$ of $\F_2^n$ such that
   \begin{equation}\label{uauh} d[U_A;U_H] \leq \tfrac{1}{2} C' \log K\end{equation}
   with $C' = 11$.
   By Lemma \ref{ruzsa-diff} we conclude that

blueprint/src/print.tex

@@ -31,7 +31,7 @@
 \input{preamble/common}
 \input{preamble/print}
 
-\title{PFR}
+\title{PFR Blueprint}
 \author{Terence Tao}
 
 \begin{document}