From f3ad1e368eb5680947ef535f00241170fb156857 Mon Sep 17 00:00:00 2001 From: teorth Date: Wed, 15 Nov 2023 12:59:11 -0800 Subject: [PATCH] Gettting blueprint to compile --- PFR/entropy_pfr.lean | 17 +++++++++++++++++ PFR/main.lean | 1 + PFR/ruzsa_distance.lean | 3 +++ blueprint/src/chapter/distance.tex | 8 ++++---- blueprint/src/chapter/pfr.tex | 4 ++-- blueprint/src/print.tex | 2 +- 6 files changed, 28 insertions(+), 7 deletions(-) create mode 100644 PFR/entropy_pfr.lean diff --git a/PFR/entropy_pfr.lean b/PFR/entropy_pfr.lean new file mode 100644 index 00000000..bc38d016 --- /dev/null +++ b/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 diff --git a/PFR/main.lean b/PFR/main.lean index 4d0bb005..4132e0df 100644 --- a/PFR/main.lean +++ b/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 diff --git a/PFR/ruzsa_distance.lean b/PFR/ruzsa_distance.lean index 59e230da..fa766e32 100644 --- a/PFR/ruzsa_distance.lean +++ b/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 diff --git a/blueprint/src/chapter/distance.tex b/blueprint/src/chapter/distance.tex index 5dfb0946..e27f90ca 100644 --- a/blueprint/src/chapter/distance.tex +++ b/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*} diff --git a/blueprint/src/chapter/pfr.tex b/blueprint/src/chapter/pfr.tex index 4ef12098..077a74f1 100644 --- a/blueprint/src/chapter/pfr.tex +++ b/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 diff --git a/blueprint/src/print.tex b/blueprint/src/print.tex index 3154fc4b..2d4546e5 100644 --- a/blueprint/src/print.tex +++ b/blueprint/src/print.tex @@ -31,7 +31,7 @@ \input{preamble/common} \input{preamble/print} -\title{PFR} +\title{PFR Blueprint} \author{Terence Tao} \begin{document}