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 $|A+A|\le K|A|$. There exists $A^{\prime }\subseteq A$ such that $|A^{\prime }|\ge K^{-17}|A|$ and $\dim A^{\prime }\le (40/\log 2)\log K$.

def IsShift {G : Type u_1} [AddCommGroup G] (A B : Set G) : Prop

A set A is a shift of a set B if it can be written as x + B.

Equations

• IsShift A B = ∃ (x : G), A = x +ᵥ B

theorem IsShift.sub_self_congr {G : Type u_1} [AddCommGroup G] {A B : Set G} : IsShift A B → A - A = B - B

theorem IsShift.card_congr {G : Type u_1} [AddCommGroup G] {A B : Set G} : IsShift A B → Nat.card ↑A = Nat.card ↑B

def NotInCoset {G : Type u_1} [AddCommGroup G] (A B : Set G) : Prop

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)) = ⊤)

theorem wlog_notInCoset {G : Type u_1} [AddCommGroup G] {A B : Set G} (hA : A.Nonempty) (hB : B.Nonempty) : ∃ (G' : AddSubgroup G) (A' : Set ↑↑G') (B' : Set ↑↑G'), IsShift A (Subtype.val '' A') ∧ IsShift B (Subtype.val '' B') ∧ NotInCoset A' B'

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.

theorem torsion_free_doubling {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableSingletonClass G] [Countable G] {Ω : Type u_2} {Ω' : Type u_3} [MeasurableSpace Ω] [MeasurableSpace Ω'] (X : Ω → G) (Y : Ω' → G) (μ : MeasureTheory.Measure Ω := by volume_tac) (μ' : MeasureTheory.Measure Ω' := by volume_tac) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] [FiniteRange X] [FiniteRange Y] (hX : Measurable X) (hY : Measurable Y) (hG : AddMonoid.IsTorsionFree G) : d[X ; μ # Y + Y ; μ'] ≤ 5 * d[X ; μ # Y ; μ']

If G is torsion-free and X, Y are G-valued random variables then d[X ; 2Y] ≤ 5d[X ; Y].

theorem torsion_dist_shrinking {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableSingletonClass G] [Countable G] {Ω : Type u_2} {Ω' : Type u_3} [MeasurableSpace Ω] [MeasurableSpace Ω'] (X : Ω → G) (Y : Ω' → G) (μ : MeasureTheory.Measure Ω := by volume_tac) (μ' : MeasureTheory.Measure Ω' := by volume_tac) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] {H : Type u_4} [FiniteRange X] [FiniteRange Y] (hX : Measurable X) (hY : Measurable Y) [AddCommGroup H] [Module (ZMod 2) H] [MeasurableSpace H] [MeasurableSingletonClass H] [Countable H] (hG : AddMonoid.IsTorsionFree G) (φ : G →+ H) : H[⇑φ ∘ X ; μ] ≤ 10 * d[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 ; μ'].

theorem app_ent_PFR' {G : Type u_1} [AddCommGroup G] [Module (ZMod 2) G] [Fintype G] [MeasurableSpace G] [MeasurableSingletonClass G] {Ω : Type u_2} {Ω' : Type u_3} [mΩ : MeasureTheory.MeasureSpace Ω] [mΩ' : MeasureTheory.MeasureSpace Ω'] (X : Ω → G) (Y : Ω' → G) [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {α : ℝ} (hent : 20 * d[X # Y] < α * (H[X] + H[Y])) (hX : Measurable X) (hY : Measurable Y) : ∃ (H : Submodule (ZMod 2) G), Real.log ↑(Nat.card ↥H) < (1 + α) / 2 * (H[X] + H[Y]) ∧ H[⇑H.mkQ ∘ X] + H[⇑H.mkQ ∘ Y] < α * (H[X] + H[Y])

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\le 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.

theorem app_ent_PFR {G : Type u_1} [AddCommGroup G] [Module (ZMod 2) G] [Fintype G] [MeasurableSpace G] [MeasurableSingletonClass G] {Ω : Type u_2} {Ω' : Type u_3} [MeasurableSpace Ω] [MeasurableSpace Ω'] (X : Ω → G) (Y : Ω' → G) (μ : MeasureTheory.Measure Ω := by volume_tac) (μ' : MeasureTheory.Measure Ω' := by volume_tac) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] (α : ℝ) (hent : 20 * d[X ; μ # Y ; μ'] < α * (H[X ; μ] + H[Y ; μ'])) (hX : Measurable X) (hY : Measurable Y) : ∃ (H : Submodule (ZMod 2) G), Real.log ↑(Nat.card ↥H) < (1 + α) / 2 * (H[X ; μ] + H[Y ; μ']) ∧ H[⇑H.mkQ ∘ X ; μ] + H[⇑H.mkQ ∘ Y ; μ'] < α * (H[X ; μ] + H[Y ; μ'])

theorem PFR_projection' {G : Type u_1} [AddCommGroup G] [Module (ZMod 2) G] [Fintype G] [MeasurableSpace G] [MeasurableSingletonClass G] {Ω : Type u_2} {Ω' : Type u_3} [MeasurableSpace Ω] [MeasurableSpace Ω'] (X : Ω → G) (Y : Ω' → G) (μ : MeasureTheory.Measure Ω := by volume_tac) (μ' : MeasureTheory.Measure Ω' := by volume_tac) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] (α : ℝ) (hX : Measurable X) (hY : Measurable Y) (αpos : 0 < α) (αone : α < 1) : ∃ (H : Submodule (ZMod 2) G), Real.log ↑(Nat.card ↥H) ≤ (1 + α) / (2 * (1 - α)) * (H[X ; μ] + H[Y ; μ']) ∧ α * (H[⇑H.mkQ ∘ X ; μ] + H[⇑H.mkQ ∘ Y ; μ']) ≤ 20 * d[⇑H.mkQ ∘ X ; μ # ⇑H.mkQ ∘ Y ; μ']

If $G={\mathbb{F}}_2^d$ and X, Y are G-valued random variables and $\alpha <1$ then there is a subgroup $H\le {\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)].]

theorem PFR_projection {G : Type u_1} [AddCommGroup G] [Module (ZMod 2) G] [Fintype G] [MeasurableSpace G] [MeasurableSingletonClass G] {Ω : Type u_2} {Ω' : Type u_3} [MeasurableSpace Ω] [MeasurableSpace Ω'] (X : Ω → G) (Y : Ω' → G) (μ : MeasureTheory.Measure Ω := by volume_tac) (μ' : MeasureTheory.Measure Ω' := by volume_tac) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] (hX : Measurable X) (hY : Measurable Y) : ∃ (H : Submodule (ZMod 2) G), Real.log ↑(Nat.card ↥H) ≤ 2 * (H[X ; μ] + H[Y ; μ']) ∧ H[⇑H.mkQ ∘ X ; μ] + H[⇑H.mkQ ∘ Y ; μ'] ≤ 34 * d[⇑H.mkQ ∘ X ; μ # ⇑H.mkQ ∘ Y ; μ']

If $G={\mathbb{F}}_2^d$ and X, Y are G-valued random variables then there is a subgroup $H\le {\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)].]

theorem four_logs {a b c d : ℝ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (hd : 0 < d) : Real.log (a * b / (c * d)) = Real.log a + Real.log b - Real.log c - Real.log d

theorem sum_prob_preimage {G : Type u_1} {H : Type u_2} {X : Finset H} {A : Set G} [Finite ↑A] {φ : ↑A → { x : H // x ∈ X }} {A_ : H → Set G} (hA : A.Nonempty) (hφ : ∀ (x : { x : H // x ∈ X }), A_ ↑x = Subtype.val '' (φ ⁻¹' {x})) : ∑ x ∈ X, ↑(Nat.card ↑(A_ x)) / ↑(Nat.card ↑A) = 1

theorem single_fibres {G : Type u_1} {H : Type u_2} {Ω : Type u_3} {Ω' : Type u_4} [AddCommGroup G] [Countable G] [MeasurableSpace G] [MeasurableSingletonClass G] [AddCommGroup H] [Countable H] [MeasurableSpace H] [MeasurableSingletonClass H] [MeasureTheory.MeasureSpace Ω] [MeasureTheory.MeasureSpace Ω'] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (φ : G →+ H) {A B : Set G} [Finite ↑A] [Finite ↑B] {UA : Ω → G} {UB : Ω' → G} (hA : A.Nonempty) (hB : B.Nonempty) (hUA' : Measurable UA) (hUB' : Measurable UB) (hUA : ProbabilityTheory.IsUniform A UA MeasureTheory.volume) (hUB : ProbabilityTheory.IsUniform B UB MeasureTheory.volume) (hUA_mem : ∀ (ω : Ω), UA ω ∈ A) (hUB_mem : ∀ (ω : Ω'), UB ω ∈ B) : ∃ (x : H) (y : H) (Ax : Set G) (By : Set G), Ax = A ∩ (↑φ).toFun ⁻¹' {x} ∧ By = B ∩ (↑φ).toFun ⁻¹' {y} ∧ Ax.Nonempty ∧ By.Nonempty ∧ d[(↑φ).toFun ∘ UA # (↑φ).toFun ∘ UB] * Real.log (↑(Nat.card ↑A) * ↑(Nat.card ↑B) / (↑(Nat.card ↑Ax) * ↑(Nat.card ↑By))) ≤ (H[(↑φ).toFun ∘ UA] + H[(↑φ).toFun ∘ UB]) * (d[UA # UB] - dᵤ[Ax # By])

Let $\varphi :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 {\varphi }^{-1}(x)$ and $B_y=B\cap {\varphi }^{-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}).]

theorem third_iso {G : Type u_2} [AddCommGroup G] {G₂ : AddSubgroup G} (H' : AddSubgroup (G ⧸ G₂)) : let H := G ⧸ G₂; let φ := QuotientAddGroup.mk' G₂; let N := AddSubgroup.comap φ H'; ∃ (e : H ⧸ H' ≃+ G ⧸ N), ∀ (x : G), e ((QuotientAddGroup.mk' H') (φ x)) = (QuotientAddGroup.mk' N) x

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

theorem single {Ω : Type u_2} [MeasurableSpace Ω] [DiscreteMeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {A : Set Ω} {z : Ω} (hA : μ.real A = 1) (hz : 0 < μ.real {z}) : z ∈ A

theorem weak_PFR_asymm_prelim {G : Type u_1} [AddCommGroup G] [Module.Free ℤ G] [Module.Finite ℤ G] [Countable G] [MeasurableSpace G] [MeasurableSingletonClass G] (A B : Set G) [A_fin : Finite ↑A] [B_fin : Finite ↑B] (hnA : A.Nonempty) (hnB : B.Nonempty) : ∃ (N : AddSubgroup G) (x : G ⧸ N) (y : G ⧸ N) (Ax : Set G) (By : Set G), Ax.Nonempty ∧ By.Nonempty ∧ Ax.Finite ∧ By.Finite ∧ Ax = {z : G | z ∈ A ∧ (QuotientAddGroup.mk' N) z = x} ∧ By = {z : G | z ∈ B ∧ (QuotientAddGroup.mk' N) z = y} ∧ Real.log 2 * ↑(Module.finrank ℤ G) ≤ Real.log ↑(Nat.card (G ⧸ N)) + 40 * dᵤ[A # B] ∧ Real.log ↑(Nat.card ↑A) + Real.log ↑(Nat.card ↑B) - Real.log ↑(Nat.card ↑Ax) - Real.log ↑(Nat.card ↑By) ≤ 34 * (dᵤ[A # B] - dᵤ[Ax # By])

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|}\le 34(d[U_A;U_B]-d[U_{A_x};U_{B_y}])$$ and one has the dimension bound $$n\log 2\le \log |G/N|+40d[U_A;U_B]$$.

def WeakPFRAsymmConclusion {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] (A B : Set G) : Prop

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.

def not_in_coset {G : Type u_2} [AddCommGroup G] (A B : Set G) : Prop

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)) = ⊤)

theorem dimension_of_shift {G : Type u_2} [AddCommGroup G] {H : AddSubgroup G} (A : Set ↥H) (x : G) : AffineSpace.finrank ℤ ((fun (a : ↥H) => ↑a + x) '' A) = AffineSpace.finrank ℤ A

In fact one has equality here, but this is trickier to prove and not needed for the argument.

theorem conclusion_transfers {G : Type u_1} [AddCommGroup G] [Countable G] [MeasurableSpace G] [MeasurableSingletonClass G] {A B : Set G} (G' : AddSubgroup G) (A' B' : Set ↑↑G') (hA : IsShift A (Subtype.val '' A')) (hB : IsShift B (Subtype.val '' B')) [Finite ↑A'] [Finite ↑B'] (hA' : A'.Nonempty) (hB' : B'.Nonempty) (h : WeakPFRAsymmConclusion A' B') : WeakPFRAsymmConclusion A B

theorem weak_PFR_asymm {G : Type u_1} [AddCommGroup G] [Module.Free ℤ G] [Module.Finite ℤ G] [Countable G] [MeasurableSpace G] [MeasurableSingletonClass G] (A B : Set G) [Finite ↑A] [Finite ↑B] (hA : A.Nonempty) (hB : B.Nonempty) : WeakPFRAsymmConclusion A B

If $A,B\subseteq {\mathbb{Z}}^d$ are finite non-empty sets then there exist non-empty $A^{\prime }\subseteq A$ and $B^{\prime }\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^{\prime },\dim B^{\prime })\le \frac{40}{\log 2}d[U_A;U_B]$.

theorem weak_PFR {G : Type u_1} [AddCommGroup G] [Module.Free ℤ G] [Module.Finite ℤ G] [Countable G] [MeasurableSpace G] [MeasurableSingletonClass G] {A : Set G} [Finite ↑A] {K : ℝ} (hA : A.Nonempty) (hK : 0 < K) (hdist : dᵤ[A # A] ≤ Real.log K) : ∃ A' ⊆ A, K ^ (-17) * ↑(Nat.card ↑A) ≤ ↑(Nat.card ↑A') ∧ ↑(AffineSpace.finrank ℤ A') ≤ 40 / Real.log 2 * Real.log K

If $A\subseteq {\mathbb{Z}}^d$ is a finite non-empty set with $d[U_A;U_A]\le \log K$ then there exists a non-empty $A^{\prime }\subseteq A$ such that $|A^{\prime }|\ge K^{-17}|A|$ and $\dim A^{\prime }\le \frac{40}{\log 2}\log K$.

theorem weak_PFR_int {G : Type u_2} [AddCommGroup G] [Module.Free ℤ G] [Module.Finite ℤ G] {A : Set G} [A_fin : Finite ↑A] (hnA : A.Nonempty) {K : ℝ} (hA : ↑(Nat.card ↑(A - A)) ≤ K * ↑(Nat.card ↑A)) : ∃ A' ⊆ A, ↑(Nat.card ↑A') ≥ K ^ (-17) * ↑(Nat.card ↑A) ∧ ↑(AffineSpace.finrank ℤ A') ≤ 40 / Real.log 2 * Real.log K

Let $A\subseteq {\mathbb{Z}}^d$ and $|A-A|\le K|A|$. There exists $A^{\prime }\subseteq A$ such that $|A^{\prime }|\ge K^{-17}|A|$ and $\dim A^{\prime }\le \frac{40}{\log 2}\log K$.