Weak PFR over the integers #
Here we use the entropic form of PFR to deduce a weak form of PFR over the integers.
Main statement #
weak_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 (40/\log 2)\log K$.
The property of two sets A, B of a group G not being contained in cosets of the same proper subgroup
Equations
- NotInCoset A B = (AddSubgroup.closure (A - A ∪ (B - B)) = ⊤)
Instances For
Without loss of generality, one can move (up to translation and embedding) any pair A, B of non-empty sets into a subgroup where they are not in a coset.
If G is torsion-free and X, Y are G-valued random variables then d[X ; 2Y] ≤ 5d[X ; Y].
If G is a torsion-free group and X, Y are G-valued random variables and
φ : G → 𝔽₂^d is a homomorphism then H[φ ∘ X ; μ] ≤ 10 * d[X; μ # Y ; μ'].
Equations
- ⋯ = ⋯
Let $G=\mathbb{F}_2^n$ and X, Y be G-valued random variables such that
[\mathbb{H}(X)+\mathbb{H}(Y)> (20/\alpha) d[X;Y],]
for some $\alpha > 0$.
There is a non-trivial subgroup $H\leq G$ such that
[\log \lvert H\rvert <(1+\alpha)/2 (\mathbb{H}(X)+\mathbb{H}(Y))] and
[\mathbb{H}(\psi(X))+\mathbb{H}(\psi(Y))< \alpha (\mathbb{H}(X)+\mathbb{H}(Y))]
where $\psi:G\to G/H$ is the natural projection homomorphism.
If $G=\mathbb{F}_2^d$ and X, Y are G-valued random variables and $\alpha < 1$ then there is
a subgroup $H\leq \mathbb{F}_2^d$ such that
[\log \lvert H\rvert \leq (1 + α) / (2 * (1 - α)) * (\mathbb{H}(X)+\mathbb{H}(Y))]
and if $\psi:G \to G/H$ is the natural projection then
[\mathbb{H}(\psi(X))+\mathbb{H}(\psi(Y))\leq 20/\alpha * d[\psi(X);\psi(Y)].]
If $G=\mathbb{F}_2^d$ and X, Y are G-valued random variables then there is
a subgroup $H\leq \mathbb{F}_2^d$ such that
[\log \lvert H\rvert \leq 2 * (\mathbb{H}(X)+\mathbb{H}(Y))]
and if $\psi:G \to G/H$ is the natural projection then
[\mathbb{H}(\psi(X))+\mathbb{H}(\psi(Y))\leq 34 * d[\psi(X);\psi(Y)].]
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 [d[\phi(U_A);\phi(U_B)]\log \frac{\lvert A\rvert\lvert B\rvert}{\lvert A_x\rvert\lvert B_y\rvert} \leq (\mathbb{H}(\phi(U_A))+\mathbb{H}(\phi(U_B)))(d(U_A,U_B)-d(U_{A_x},U_{B_y}).]
Move to Mathlib? Finsupp.mapRange of a surjective function is surjective.
A free Z-module is torsion-free. Move to Mathlib?
If G is a rank n free Z-module, then G/2G is a finite elementary 2-group of cardinality 2^n. Code is slow, needs to be golfed
A version of the third isomorphism theorem: if G₂ ≤ G and H' is a subgroup of G⧸G₂, then there is a canonical isomorphism between H⧸H' and G⧸N, where N is the preimage of H' in G. A bit clunky; may be a better way to do this
Given two non-empty finite subsets A, B of a rank n free Z-module G, there exists a subgroup N and points x, y in G/N such that the fibers Ax, By of A, B over x, y respectively are non-empty, one has the inequality $$\log\frac{|A| |B|}{|A_x| |B_y|} ≤ 34 (d[U_A; U_B] - d[U_{A_x}; U_{B_y}])$$ and one has the dimension bound $$n \log 2 ≤ \log |G/N| + 40 d[U_A; U_B]$$.
Separating out the conclusion of weak_PFR_asymm for convenience of induction arguments.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The property of two sets A,B of a group G not being contained in cosets of the same proper subgroup
Equations
- not_in_coset A B = (AddSubgroup.closure (A - A ∪ (B - B)) = ⊤)
Instances For
In fact one has equality here, but this is tricker to prove and not needed for the argument.
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 [\log\frac{\lvert A\rvert\lvert B\rvert}{\lvert A'\rvert\lvert B'\rvert}\leq 34 d[U_A;U_B]] such that $\max(\dim A',\dim B')\leq \frac{40}{\log 2} d[U_A;U_B]$.
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 $\lvert A'\rvert\geq K^{-17}\lvert A\rvert$ and $\dim A'\leq \frac{40}{\log 2} \log K$.
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$.