Sketched how entropy decrement => entropic PFR

PFR/100_percent.lean

@@ -0,0 +1,8 @@
+/-!
+# The 100% version of entropic PFR
+
+Here we show entropic PFR in the case of doubling constant zero.
+-/
+
+/-- If $d[X_1;X_2]=0$, then there exists a subgroup $H \leq G$ such that $d[X_1;U_H] = d[X_2;U_H] = 0$. -/
+theorem dist_eq_zero_iff : 0 = 1 := by sorry

PFR/entropy_pfr.lean

@@ -12,6 +12,36 @@ Here we prove the entropic version of the polynomial Freiman-Ruzsa conjecture.
 
 -/
 
+variable {Ω_0 Ω'_0 : Type*} [mΩ_0 : MeasurableSpace Ω_0] (μ_0 : Measure Ω_0) [mΩ'_0 : MeasurableSpace Ω'_0] (μ'_0 : Measure Ω'_0)
+
+variable {Ω Ω' Ω'' Ω''' : Type*} [mΩ : MeasurableSpace Ω] (μ : Measure Ω) [mΩ' : MeasurableSpace Ω'] (μ' : Measure Ω') [mΩ'' : MeasurableSpace Ω''] (μ'' : Measure Ω'') [mΩ''' : MeasurableSpace Ω'''] (μ''' : Measure Ω''')
+
+variable [AddCommGroup G] [ElementaryAddGroup G 2] [Fintype G]
+
+variable (X_0_1: Ω_0 → G) (X_0_2: Ω'_0 → G)
+(X_1: Ω → G) (X_2: Ω' → G)
+
+def eta := (9:ℝ)⁻¹
+
+/-- If $X_1,X_2$ are two $G$-valued random variables, then
+$$  \tau[X_1; X_2] \coloneqq d[X_1; X_2] + \eta  d[X^0_1; X_1] + \eta d[X^0_2; X_2].$$ --/
+def tau (X_1: Ω → G) (X_2 : Ω' → G) : ℝ := sorry
+
+/-- If $X'_1, X'_2$ are copies of $X_1,X_2$, then $\tau[X'_1;X'_2] = \tau[X_1;X_2]$. --/
+lemma tau_of_copy : 0 = 1 := sorry
+
+/--  There exist $G$-valued random variables $X_1, X_2$ such that
+  $$\tau[X_1;X_2] \leq \tau[X'_1;X'_2]
+  $$
+for all $G$-valued random variables $X'_1, X'_2$.-/
+lemma tau_min_exists : 0 = 1 := sorry
+
+
+
+
+/-- If $d[X_1;X_2] > 0$ then  there are $G$-valued random variables $X'_1, X'_2$ such that
+$$ \tau[X'_1;X'_2] < \tau[X_1;X_2].$$ -/
+theorem tau_strictly_decreases : 0 = 1 := sorry
 
 /-- `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

blueprint/src/chapter/100_percent.tex

@@ -0,0 +1,13 @@
+\chapter{The 100\% version of PFR}
+
+\begin{lemma}\label{lem:100pc}
+  \uses{ruz-dist-def}
+  \lean{dist_eq_zero_iff}
+  Suppose that $X_1,X_2$ are $G$-valued random variables such that
+  $d[X_1;X_2]=0$. Then there exists a subgroup $H \leq G$ such that $d[X_1;U_H] = d[X_2;U_H] = 0$.
+\end{lemma}
+
+\begin{proof} {\bf This proof will need to be deconstructed further, for instance by reading the proof in the cited paper.}
+  By the triangle inequality, $\dist{X_1}{X_1} = 0$, and so (since $G=\F_2^n$) we have $\dist{X_1}{-X_1} = 0$. By Theorem 1.11(i) of {\tt https://arxiv.org/abs/0906.4387} it follows that there exists a subgroup $H$ with $\dist{X_1}{U_H} = 0$.
+  Then $\dist{X_2}{U_H}=0$ follows by the triangle inequality.
+\end{proof}

blueprint/src/chapter/main.tex

@@ -5,5 +5,6 @@
 \input{chapter/jensen}
 \input{chapter/entropy}
 \input{chapter/distance}
+\input{chapter/100_percent}
 \input{chapter/pfr-entropy}
 \input{chapter/pfr}

blueprint/src/chapter/pfr-entropy.tex

@@ -1,7 +1,58 @@
 \chapter{Entropy version of PFR}
 
+\begin{definition}\label{eta-def}
+ \lean{eta}\leanok
+  $\eta := 1/9$.
+\end{definition}
+
+Throughout this chapter,  $G = \F_2^n$, and $X^0_1, X^0_2$ are $G$-valued random variables.
+
+\begin{definition}[$\tau$ functional]\label{tau-def}
+  \uses{eta-def}
+  \lean{tau}
+If $X_1,X_2$ are two $G$-valued random variables, then
+$$  \tau[X_1; X_2] \coloneqq \dist{X_1}{X_2} + \eta  \dist{X^0_1}{X_1} + \eta \dist{X^0_2}{X_2}.$$
+\end{definition}
+
+\begin{lemma}[$\tau$ depends only on distribution]\label{tau-copy}
+  \uses{tau-def}
+  \lean{tau-copy}  If $X'_1, X'_2$ are copies of $X_1,X_2$, then $\tau[X'_1;X'_2] = \tau[X_1;X_2]$.
+\end{lemma}
+
+
+\begin{proof}\uses{copy-ent} Immediate from Lemma \ref{copy-ent}.
+\end{proof}
+
+
+
+
+\begin{theorem}[$\tau$-decrement]\label{de-prop}
+  \uses{tau-def, ruz-dist-def}
+  \lean{tau-strictly-decreases}
+  Let $X_1, X_2$ be two $G$-valued random variables with $d[X_1;X_2] > 0$. Then there are $G$-valued random variables $X'_1, X'_2$ such that
+$$\tau[X'_1;X'_2] < \tau[X_1;X_2].
+$$
+\end{theorem}
+
+\begin{proof}  Sorry!  This is hard!
+\end{proof}
+
+
+\begin{proposition}[$\tau$ has minimum]\label{tau-min}\uses{tau-def}
+  \lean{tao-min-exists}
+  There exist $G$-valued random variables $X_1, X_2$ such that
+  $$\tau[X_1;X_2] \leq \tau[X'_1;X'_2]
+  $$
+for all $G$-valued random variables $X'_1, X'_2$.
+\end{proposition}
+
+\begin{proof} By Lemma \ref{tau-copy}, $\tau$ only depends on the probability distributions of $X_1, X_2$. This ranges over a compact space, and $\tau$ is continuous.  So $\tau$ has a minimum.
+\end{proof}
+
+
 
 \begin{theorem}[Entropy version of PFR]\label{entropy-pfr}\uses{ruz-dist-def}
+  \lean{entropic_PFR_conjecture}
   Let $G = \F_2^n$, and suppose that $X^0_1, X^0_2$ are $G$-valued random variables.
   Then there is some subgroup $H \leq G$ such that
   \[
@@ -13,5 +64,5 @@ \chapter{Entropy version of PFR}
 
 Probably need a definition for a uniform distribution on a non-empty subset $H$ of a set $S$.
 
-\begin{proof} Sorry!
+\begin{proof} \uses{de-prop, tau-min, lem:100pc, ruzsa-triangle}  Let $X_1, X_2$ be the minimizer from Lemma \ref{tau-min}.  From Theorem \ref{de-prop}, $d[X_1;X_2]=0$.  From Lemma \ref{lem:100pc}, $d[X_1;U_H] = d[X_2; U_H] = 0$.  Also from minimization we have $\tau[X_1;X_2] \leq \tau[X^0_1;X^0_2]$.  Using this and the Ruzsa triangle inequality we can conclude.
 \end{proof}