Blueprint of first estimate

PFR/first-estimate.lean

@@ -15,3 +15,8 @@ Assumptions (need to be placed explicitly in the file):
 
 /--  We have $I_1 \leq 2 \eta k$ -/
 lemma first_estimate : 0 = 1 := by sorry
+
+
+/--     H[X_1+X_2+\tilde X_1+\tilde X_2] \le \tfrac{1}{2} H[X_1]+\tfrac{1}{2} H[X_2] + (2 + \eta) k - I_1.
+-/
+lemma ent_ofsum_le : 0 = 1 := by sorry

PFR/ruzsa_distance.lean

@@ -86,3 +86,20 @@ lemma ent_bsg : 0 = 1 := by sorry
 
 
 end Balog_Szemeredi_Gowers
+
+
+/--   Suppose that $(X, Z)$ and $(Y, W)$ are random variables, where $X, Y$ take values in an abelian group. Then
+$$   d[X  | Z;Y | W] \leq d[X; Y] + \tfrac{1}{2} I[X : Z] + \tfrac{1}{2} I[Y : W].$$
+-/
+lemma condDist_le : 0 = 1 := by sorry
+
+
+/-- Let $X, Y, Z$ be random variables taking values in some abelian group, and with $Y, Z$ independent. Then we have
+  $$ d[X; Y + Z] -d[X; Y]  \leq \tfrac{1}{2} (H[Y+Z] - H[Y]) $$
+  $$ = \tfrac{1}{2} d[Y; Z] + \tfrac{1}{4} H[Z] - \tfrac{1}{4} H[Y]$$
+  and
+$$
+  d[X;Y|Y+Z] - d[X;Y] \leq \tfrac{1}{2} \bigl(H[Y+Z] - H[Z]\bigr) $$
+   = \tfrac{1}{2} d[Y;Z] + \tfrac{1}{4} H[Y] - \tfrac{1}{4} H[Z].
+-/
+lemma condDist_le' : 0 = 1 := by sorry

blueprint/src/chapter/distance.tex

@@ -258,3 +258,45 @@ \chapter{Ruzsa calculus}
 and similarly for $\bbH[B_2 | Z]$, we see that~\eqref{lhs-to-bound} is bounded by
 $3I[A:B] + 2H[Z]-H[A]-H[B]$ as claimed.
 \end{proof}
+
+
+\begin{lemma}\label{cond-dist-fact}
+  \uses{cond-ruz-dist, information-def}
+  \lean{condDist_le}
+  Suppose that $(X, Z)$ and $(Y, W)$ are random variables, where $X, Y$ take values in an abelian group. Then
+  \[    d[X  | Z;Y | W] \leq d[X; Y] + \tfrac{1}{2} I[X : Z] + \tfrac{1}{2} I[Y : W].\]
+\end{lemma}
+
+\begin{proof}
+\uses{cond-dist-alt, independent-exist, cond-reduce}
+Using Lemma \ref{cond-dist-alt} and Lemma \ref{independent-exist}, if $(X',Z'), (Y',W')$ are independent copies of the variables $(X,Z)$, $(Y,W)$, we have
+\begin{align*}
+  d[X  | Z; Y | W]&= H[X'-Y'|Z',W'] - \tfrac{1}{2} H[X'|Z'] - \tfrac{1}{2}H[Y'|W'] \\
+                       &\le H[X'-Y']- \tfrac{1}{2} H[X'|Z'] - \tfrac{1}{2}H[Y'|W'] \\
+                       &= d[X';Y'] + \tfrac{1}{2} I[X' : Z'] + \tfrac{1}{2} I[Y' : W'].
+\end{align*}
+Here, in the middle step we used Lemma \ref{cond-reduce}, and in the last step we used Definition \ref{ruz-dist-def} and Definition \ref{information-def}.
+\end{proof}
+
+\begin{lemma}\label{first-useful}
+  \uses{independent-def, ruz-dist-def, cond-dist-def, entropy-def, conditional-entropy-def}
+  \lean{condDist_le'}
+  Let $X, Y, Z$ be random variables taking values in some abelian group, and with $Y, Z$ independent. Then we have
+  \begin{align}\nonumber d[X; Y + Z] -d[X; Y] &  \leq \tfrac{1}{2} (H[Y+Z] - H[Y]) \\ & = \tfrac{1}{2} d[Y; Z] + \tfrac{1}{4} H[Z] - \tfrac{1}{4} H[Y]. \label{lem51-a} \end{align}
+  and
+  \begin{align}\nonumber
+  d[X;Y|Y+Z] - d[X;Y] & \leq \tfrac{1}{2} \bigl(H[Y+Z] - H[Z]\bigr) \\ & = \tfrac{1}{2} d[Y;Z] + \tfrac{1}{4} H[Y] - \tfrac{1}{4} H[Z].
+    \label{ruzsa-3}
+  \end{align}
+  \end{lemma}
+
+  \begin{proof}
+    \uses{ruz-copy, ruz-lean, independent-exist, kv, ruz-indep, relabeled-entropy, cond-dist-fact}
+  We first prove~\eqref{lem51-a}. We may assume (taking an independent copy, using Lemma \ref{independent-exist} and Lemma \ref{ruz-copy}, \ref{ruz-ent}) that $X$ is independent of $Y, Z$. Then we have
+  \begin{align*}  d[X;Y+Z] & - d[X;Y] \\ & = H[X + Y + Z] - H[X+Y] - \tfrac{1}{2}H[Y + Z] + \tfrac{1}{2} H[Y].\end{align*}
+  Combining this with Lemma \ref{kv} gives the required bound. The second form of the result is immediate Lemma \ref{ruz-indep}.
+
+  Turning to~\eqref{ruzsa-3}, we have from Definition \ref{information-def} and Lemma \ref{relabeled-entropy}
+  \begin{align*} I[Y : Y+Z] & = H[Y] + H[Y + Z] - H[Y, Y + Z] \\ & = H[Y] + H[Y + Z] - H[Y, Z]  = H[Y + Z] - H[Z],\end{align*}
+  and so~\eqref{ruzsa-3} is a consequence of Lemma \ref{cond-dist-fact}. Once again the second form of the result is immediate from Lemma \ref{ruz-indep}.
+\end{proof}

blueprint/src/chapter/pfr-entropy.tex

@@ -81,7 +81,7 @@ \subsection{First estimate}
   \lean{first-estimate} We have $I_1 \leq 2 \eta k$.
 \end{lemma}
 
-\begin{proof}\uses{cor-fibre, distance-lower, cor-distance-lower}  From Corollary \ref{cor-fibre} we have
+\begin{proof}\uses{cor-fibre, distance-lower, cor-distance-lower, first-useful}  From Corollary \ref{cor-fibre} we have
   \begin{align*}
     &   d[X_1+\tilde X_2;X_2+\tilde X_1] + d[X_1|X_1+\tilde X_2; X_2|X_2+\tilde X_1] \\
     &\quad + I[ X_1+ X_2 : \tilde X_1 + X_2 \,|\, X_1 + X_2 + \tilde X_1 + \tilde X_2 ] = 2k.
@@ -103,9 +103,38 @@ \subsection{First estimate}
 &\qquad \qquad +(d[X_1^0;X_1|X_1+\tilde X_2]-d[X_1^0;X_1]) \nonumber \\ & \qquad \qquad \qquad \qquad  +(d\dist[X_2^0; X_2|X_2+\tilde X_1]-d[X_2^0;X_2]) \leq 2k.
 \label{suff-for-first-est}
 \end{align}
-...
+
+By Lemma \ref{first-useful} (and recalling that $k$ is defined to be $d[X_1;X_2]$) we have
+\[ d[X^0_1; X_1+\tilde X_2] - d[X^0_1; X_1] \leq \tfrac{1}{2} k + \tfrac{1}{4} H[X_2] - \tfrac{1}{4} H[X_1],\] \[  d[X^0_2;X_2+\tilde X_1] - d[X^0_2; X_2] \leq \tfrac{1}{2} k + \tfrac{1}{4} H[X_1] - \tfrac{1}{4} H[X_2],\]
+\begin{equation}  d[X_1^0;X_1|X_1+\tilde X_2] - \dist[X_1^0;X_1] \leq \tfrac{1}{2} k + \tfrac{1}{4} H[X_1] - \tfrac{1}{4} H[X_2]                                 \label{second-dist1}
+\end{equation}
+and
+\begin{equation}
+  \label{second-dist2}
+  d[X_2^0; X_2|X_2+\tilde X_1] - d[X_2^0; X_2] \leq \tfrac{1}{2}k + \tfrac{1}{4} H[X_2] - \tfrac{1}{4} H[X_1].
+\end{equation}
+Adding all these inequalities, we obtain~\eqref{suff-for-first-est}.
+\end{proof}
+
+\begin{lemma}\label{foursum-bound}
+  \uses{entropy-def}
+  \lean{ent_ofsum_le}
+  With the same notation, we have
+  \begin{equation}
+    \label{HS-bound}
+    H[X_1+X_2+\tilde X_1+\tilde X_2] \le \tfrac{1}{2} H[X_1]+\tfrac{1}{2} H[X_2] + (2 + \eta) k - I_1.
+  \end{equation}
+\end{lemma}
+
+\begin{proof}\uses{first-estimate, ruz-indep}
+  Subtracting~\eqref{second-tc2} from~\eqref{second-main}, and combining the resulting inequality with~\eqref{second-dist1} and~\eqref{second-dist2} (Note: these should all be extracted as separate lemmas) gives the bound
+\[
+  \dist{X_1+\tilde X_2}{X_2+\tilde X_1} \le (1 + \eta) k - I_1,
+\]
+and the claim follows from Lemma \ref{ruz-indep}.
 \end{proof}
 
+
 \subsection{Second estimate}
 
 ...