Weak PFR over the integers
Lemmatorsion-free-doubling#
If \(G\) is torsion-free and \(X,Y\) are \(G\)-valued random variables then \(d[X;2Y]\leq 5d[X;Y]\).
Proof
Let \(Y_1,Y_2\) be independent copies of \(Y\) (also independent of \(X\)). Since \(G\) is torsion-free we know \(X,Y_1-Y_2,X-2Y_1\) uniquely determine \(X,Y_1,Y_2\) and so
Similarly
Furthermore
By submodularity (Alternate form of submodularity)
Combining these inequalities
Similarly we have
and
and by submodularity (Alternate form of submodularity) again
Combining these inequalities (and recalling the definition of Ruzsa distance) gives
It follows that
and so (using \(\mathbb{H}(2Y)=\mathbb{H}(Y)\))
Finally note that by the triangle inequality (Ruzsa triangle inequality) we have
The result follows from \((\mathbb{H}(Y)-\mathbb{H}(X))/2\leq d[X;Y]\) (Distance controls entropy difference).
Lean
Formalized as torsion_free_doubling.
Sources
Uses 3 · Used by 1
Lemmatorsion-dist-shrinking#
If \(G\) is a torsion-free group and \(X,Y\) are \(G\)-valued random variables and \(\phi:G\to \mathbb{F}_2^d\) is a homomorphism then
Proof
By Corollary fibring-ineq and Lemma torsion-free-doubling we have
and \(\phi(2Y)=2\phi(Y)\equiv 0\) so the left-hand side is equal to \(d[\phi(X);0]=\mathbb{H}(\phi(X))/2\) (using Distance from zero).
Lean
Formalized as torsion_dist_shrinking.
Sources
Uses 3 · Used by 1
Lemmaapp-ent-pfr#
Let \(G=\mathbb{F}_2^n\) and \(\alpha\in (0,1)\) and let \(X,Y\) be \(G\)-valued random variables such that
There is a non-trivial subgroup \(H\leq G\) such that
and
where \(\psi:G\to G/H\) is the natural projection homomorphism.
Proof
By Improved entropy version of PFR there exists a subgroup \(H\) such that \(d[X;U_H] + d[Y;U_H] \leq 10 d[X;Y]\). Using Projection entropy and distance we deduce that \(\mathbb{H}(\psi(X)) + \mathbb{H}(\psi(X)) \leq 20 d[X;Y]\). The second claim follows adding these inequalities and using the assumption on \(\mathbb{H}(X)+\mathbb{H}(Y)\).
Furthermore we have by Distance controls entropy difference
and similarly for \(Y\) and thus
Finally note that if \(H\) were trivial then \(\psi(X)=X\) and \(\psi(Y)=Y\) and hence \(\mathbb{H}(X)+\mathbb{H}(Y)=0\), which contradicts Distance nonnegative.
Lean
Formalized as app_ent_PFR.
Sources
Uses 4 · Used by 1
Lemmapfr-projection'#
If \(G=\mathbb{F}_2^d\) and \(\alpha\in (0,1)\) and \(X,Y\) are \(G\)-valued random variables then there is a subgroup \(H\leq \mathbb{F}_2^d\) such that
and if \(\psi:G \to G/H\) is the natural projection then
Proof
Let \(H\leq \mathbb{F}_2^d\) be a maximal subgroup such that
and such that there exists \(c \ge 0\) with
and
Note that this exists since \(H=\{0\}\) is an example of such a subgroup or we are done with this choice of \(H\).
We know that \(G/H\) is a \(2\)-elementary group and so by Lemma app-ent-pfr there exists some non-trivial subgroup \(H'\leq G/H\) such that
and
where \(\psi':G/H\to (G/H)/H'\). By group isomorphism theorems we know that there exists some \(H''\) with \(H\leq H''\leq G\) such that \(H'\cong H''/H\) and \(\psi' \circ \psi(X)=\psi''(X)\) where \(\psi'':G\to G/H''\) is the projection homomorphism.
Since \(H'\) is non-trivial we know that \(H\) is a proper subgroup of \(H''\). On the other hand we know that
and
Therefore (using the maximality of \(H\)) it must be the first condition that fails, whence
Lean
Formalized as PFR_projection'.
Sources
Uses 1 · Used by 1
We could use the previous lemma for any value of \(\alpha \in (0,1)\), which would give a whole range of estimates in Theorem weak-pfr-int. For definiteness, we specialize only to \(\alpha=3/5\), which gives a constant \(2\) in the first bound below.
Lemmapfr-projection#
If \(G=\mathbb{F}_2^d\) and \(\alpha\in (0,1)\) and \(X,Y\) are \(G\)-valued random variables then there is a subgroup \(H\leq \mathbb{F}_2^d\) such that
and if \(\psi:G \to G/H\) is the natural projection then
Proof
Specialize Lemma pfr-projection' to \(\alpha=3/5\). In the second inequality, it gives a bound \(100/3 < 34\).
Lean
Formalized as PFR_projection.
Sources
Uses 1 · Used by 1
Lemmasingle-fibres#
Let \(\phi:G\to H\) be a homomorphism and \(A,B\subseteq G\) be finite subsets. If \(x,y\in H\) then let \(A_x=A\cap \phi^{-1}(x)\) and \(B_y=B\cap \phi^{-1}(y)\). There exist \(x,y\in H\) such that \(A_x,B_y\) are both non-empty and
Proof
The random variables \((U_A\mid \phi(U_A)=x)\) and \((U_B\mid \phi(U_B)=y)\) are equal in distribution to \(U_{A_x}\) and \(U_{B_y}\) respectively (both are uniformly distributed over their respective fibres). It follows from General fibring identity that
Therefore with \(M:=\mathbb{H}(\phi(U_A))+\mathbb{H}(\phi(U_B))\) we have
Since
we have
It follows that there exists some \(x,y\in H\) such that \(\lvert A_x\rvert,\lvert B_y\rvert\neq 0\) and
Lean
Formalized as single_fibres.
Sources
Uses 1 · Used by 1
Definitiondimension-def#
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'}\).
Used by 3
Theoremweak-pfr-asymm#
If \(A,B\subseteq \mathbb{Z}^d\) are finite non-empty sets then there exist non-empty \(A'\subseteq A\) and \(B'\subseteq B\) such that
such that \(\max(\dim A',\dim B')\leq \frac{40}{\log 2} d[U_A;U_B]\).
Proof
Without loss of generality we can assume that \(A\) and \(B\) are not both inside (possibly distinct) cosets of the same subgroup of \(\mathbb{Z}^d\), or we just replace \(\mathbb{Z}^d\) with that subgroup. We prove the result by induction on \(\lvert A\rvert+\lvert B\rvert\).
Let \(\phi:\mathbb{Z}^d\to \mathbb{F}_2^d\) be the natural mod-2 homomorphism. By Lemma torsion-dist-shrinking
We now apply Lemma pfr-projection, obtaining some subgroup \(H\leq \mathbb{F}_2^d\) such that
and
where \(\tilde{\phi}:\mathbb{Z}^d\to \mathbb{F}_2^d/H\) is \(\phi\) composed with the projection onto \(\mathbb{F}_2^d/H\).
By Lemma single-fibres there exist \(x,y\in \mathbb{F}_2^d/H\) such that, with \(A_x=A\cap \tilde{\phi}^{-1}(x)\) and similarly for \(B_y\),
Suppose first that \(\lvert A_x\rvert+\lvert B_y\rvert=\lvert A\rvert+\lvert B\rvert\). This means that \(\tilde{\phi}(A)=\{x\}\) and \(\tilde{\phi}(B)=\{y\}\), and hence both \(A\) and \(B\) are in cosets of \(\ker \tilde{\phi}\). Since by assumption \(A,B\) are not in cosets of a proper subgroup of \(\mathbb{Z}^d\) this means \(\ker\tilde{\phi}=\mathbb{Z}^d\), and so (examining the definition of \(\tilde{\phi}\)) we must have \(H=\mathbb{F}_2^d\). Then our bound on \(\log\lvert H\rvert\) forces \(d\leq \frac{40}{\log 2}d[U_A;U_B]\) and we are done with \(A'=A\) and \(B'=B\).
Otherwise,
By induction we can find some \(A'\subseteq A_x\) and \(B'\subseteq B_y\) such that \(\dim A',\dim B'\leq \frac{40}{\log 2} d[U_{A_x};U_{B_y}]\leq \frac{40}{\log 2}d[U_A;U_B]\) and
Adding these inequalities implies
as required.
Lean
Formalized as weak_PFR_asymm.
Sources
Uses 4 · Used by 1
Theoremweak-pfr-symm#
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
and \(\dim A'\leq \frac{40}{\log 2} \log K\).
Proof
Immediate from Theorem weak-pfr-asymm and rearranging.
Lean
Formalized as weak_PFR.
Sources
Uses 2 · Used by 1
Theoremweak-pfr-int#
Let \(A\subseteq \mathbb{Z}^d\) and \(\lvert A-A\rvert\leq K\lvert A\rvert\). There exists \(A'\subseteq A\) such that \(\lvert A'\rvert \geq K^{-17}\lvert A\rvert\) and \(\dim A' \leq \frac{40}{\log 2}\log K\).
Proof
As in the beginning of PFR the doubling condition forces \(d[U_A;U_A]\leq \log K\), and then we apply Theorem weak-pfr-symm.
Lean
Formalized as weak_PFR_int.
Sources
Uses 2 · Used by 1
Corollaryweak-pfr-int-sumset#
Let \(A\subseteq \mathbb{Z}^d\) and \(\lvert A+A\rvert\leq K\lvert A\rvert\). There exists \(A'\subseteq A\) such that \(\lvert A'\rvert \geq K^{-34}\lvert A\rvert\) and \(\dim A' \leq \frac{80}{\log 2}\log K\).
Proof
By the Ruzsa triangle inequality one has \(\lvert A-A\rvert \leq K^2 \lvert A\rvert\), and then we apply Theorem weak-pfr-int.
Lean
Formalized as weak_PFR_int_sumset.
Sources
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.