Skip to content

Commit

Permalink
[wip] feat: approx_hom_pfr
Browse files Browse the repository at this point in the history
  • Loading branch information
@llllvvuu
llllvvuu committed Jan 13, 2024
1 parent 43767d2 commit a52bc5b
Show file tree
Hide file tree
Showing 4 changed files with 223 additions and 20 deletions.
210 changes: 204 additions & 6 deletions PFR/ApproxHomPFR.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ import PFR.HomPFR
import Mathlib.Combinatorics.Additive.Energy
import Mathlib.Analysis.NormedSpace.PiLp
import Mathlib.Analysis.InnerProductSpace.PiL2
import PFR.ForMathlib.Graph

/-!
# The approximate homomorphism form of PFR
Expand Down Expand Up @@ -145,12 +146,209 @@ def C₄ := 4
/-- Let $G$ be an abelian group, and let $A$ be a finite non-empty set with $E(A) \geq |A|^3 / K$ for some $K \geq 1$. Then there is a subset $A'$ of $A$ with $|A'| \geq |A| / (C_1 K^{C_2})$ and $|A'-A'| \leq C_3 K^{C_4} |A'|$ -/
lemma bsg (A : Finset G) (K : ℝ) (hK: 0 < K) (hE: E[A] ≥ (A.card)^3 / K): ∃ A' : Finset G, A' ⊆ A ∧ A'.card ≥ A.card / (C₁ * K^C₂) ∧ (A' - A').card ≤ C₃ * K^C₄ * A'.card := sorry


open scoped BigOperators
variable {G G' : Type*} [AddCommGroup G] [Fintype G] [AddCommGroup G'] [Fintype G']
[ElementaryAddCommGroup G 2] [ElementaryAddCommGroup G' 2]

/-- Let $G,G'$ be finite abelian $2$-groups.
Let $f: G \to G'$ be a function, and suppose that there are at least $|G|^2 / K$ pairs $(x,y) \in G^2$ such that
$$ f(x+y) = f(x) + f(y).$$
Then there exists a homomorphism $\phi: G \to G'$ and a constant $c \in G'$ such that $f(x) = \phi(x)+c$ for at least $|G| / 4C_1^{21} C_3^{20} K^{46C_4+44 C_2}$ values of $x \in G$. -/
theorem approx_hom_pfr (f : G → G') (K : ℝ) (hK: K > 0) (hf: Nat.card { x : G × G| f (x.1+x.2) = (f x.1) + (f x.2) } ≥ (Nat.card G)^2/ K) : ∃ (φ : G →+ G') (c : G'), Nat.card { x : G | f x = φ x + c } ≥ (Nat.card G) / (4 * C₁^21 * C₃^20 * K^(46 * C₄ + 44 * C₂)) := sorry
lemma equiv_filter_graph (f : G → G') :
let A := (Set.graph f).toFinite.toFinset
(A ×ˢ A).filter (fun (a, a') ↦ a + a' ∈ A) ≃
{ x : G × G | f (x.1 + x.2) = (f x.1) + (f x.2) } where
toFun := fun ⟨a, ha⟩ ↦ by
let A := (Set.graph f).toFinite.toFinset
use (a.1.1, a.2.1)
apply Finset.mem_filter.mp at ha
have h {a} (h' : a ∈ A) := (Set.mem_graph _).mp <| (Set.graph f).toFinite.mem_toFinset.mp h'
show f (a.1.1 + a.2.1) = (f a.1.1) + (f a.2.1)
rw [h (Finset.mem_product.mp ha.1).1, h (Finset.mem_product.mp ha.1).2]
exact h ha.2
invFun := fun ⟨a, ha⟩ ↦ by
use ((a.1, f a.1), (a.2, f a.2))
refine Finset.mem_filter.mpr ⟨Finset.mem_product.mpr ⟨?_, ?_⟩, ?_⟩
<;> apply (Set.graph f).toFinite.mem_toFinset.mpr
· exact ⟨a.1, rfl⟩
· exact ⟨a.2, rfl⟩
· exact (Set.mem_graph _).mpr ha
left_inv := fun ⟨x, hx⟩ ↦ by
apply Subtype.ext
show ((x.1.1, f x.1.1), x.2.1, f x.2.1) = x
obtain ⟨hx1, hx2⟩ := Finset.mem_product.mp (Finset.mem_filter.mp hx).1
rewrite [(Set.graph f).toFinite.mem_toFinset] at hx1 hx2
rw [(Set.mem_graph x.1).mp hx1, (Set.mem_graph x.2).mp hx2]
right_inv := fun _ ↦ rfl

set_option maxHeartbeats 400000 in
/-- Let $G, G'$ be finite abelian $2$-groups.
Let $f: G \to G'$ be a function, and suppose that there are at least
$|G|^2 / K$ pairs $(x,y) \in G^2$ such that $$ f(x+y) = f(x) + f(y).$$
Then there exists a homomorphism $\phi: G \to G'$ and a constant $c \in G'$ such that
$f(x) = \phi(x)+c$ for at least $|G| / C_1 C_3^{12} K^{24C_4 + 2C_2}$ values of $x \in G$. -/
theorem approx_hom_pfr (f : G → G') (K : ℝ) (hK: K > 0)
(hf: Nat.card { x : G × G | f (x.1+x.2) = (f x.1) + (f x.2) } ≥ (Nat.card G)^2 / K) :
∃ (φ : G →+ G') (c : G'), Nat.card { x : G | f x = φ x + c } ≥
(Nat.card G) / (C₁ * C₃^12 * K^(24 * C₄ + 2 * C₂)) := by
let A := (Set.graph f).toFinite.toFinset

have h_cs : ((A ×ˢ A).filter (fun (a, a') ↦ a + a' ∈ A) |>.card : ℝ) ^ 2 ≤
Finset.card A * E[A] := by norm_cast; convert cauchy_schwarz A A
rewrite [← Nat.card_eq_finsetCard, ← Nat.card_eq_finsetCard,
Nat.card_congr (equiv_filter_graph f)] at h_cs

have hA : Nat.card A = Nat.card G := by
rewrite [← Set.card_graph f, Nat.card_eq_finsetCard, Set.Finite.card_toFinset]; simp
have hA_pos : 0 < (Nat.card A : ℝ) := Nat.cast_pos.mpr <| Nat.card_pos.trans_eq hA.symm
have : ((Nat.card G)^2 / K)^2 ≤ Nat.card A * E[A] := LE.le.trans (by gcongr) h_cs
rewrite [← hA] at this
replace : E[A] ≥ (Finset.card A)^3 / K^2 := calc
_ ≥ ((Nat.card A)^2 / K)^2 / Nat.card A := (div_le_iff' <| hA_pos).mpr this
_ = ((Nat.card A)^4 / (Nat.card A)) / K^2 := by ring
_ = (Finset.card A)^3 / K^2 := by
rw [pow_succ, mul_comm, mul_div_assoc, div_self (ne_of_gt hA_pos), mul_one,
Nat.card_eq_finsetCard]
obtain ⟨A', hA', hA'1, hA'2⟩ := bsg A (K^2) (sq_pos_of_pos hK) (by convert this)
clear h_cs this

let A'' := A'.toSet
have hA''_coe : Nat.card A'' = Finset.card A' := Nat.card_eq_finsetCard A'
have h_pos1 : 0 < (C₁ : ℝ) * (K ^ 2) ^ C₂ :=
mul_pos (by unfold C₁; norm_num) (pow_pos (pow_pos hK 2) C₂)
have hA''_pos : 0 < Nat.card A'' := by
rewrite [hA''_coe, ← Nat.cast_pos (α := ℝ)]
exact LT.lt.trans_le (div_pos (by rwa [← Nat.card_eq_finsetCard]) h_pos1) hA'1
have hA''_nonempty : Set.Nonempty A'' := nonempty_subtype.mp (Finite.card_pos_iff.mp hA''_pos)
have : Finset.card (A' - A') = Nat.card (A'' + A'') := calc
_ = Nat.card (A' - A').toSet := (Nat.card_eq_finsetCard _).symm
_ = Nat.card (A'' + A'') := by rw [Finset.coe_sub, sumset_eq_sub]
replace : Nat.card (A'' + A'') ≤ C₃ * (K ^ 2) ^ C₄ * (Nat.card A'') := by
rewrite [← this, hA''_coe]
convert hA'2
obtain ⟨H, c, hc_card, hH_le, hH_ge, hH_cover⟩ := PFR_conjecture_improv_aux hA''_nonempty this
clear hA'2 hH_le hH_ge hA_pos
obtain ⟨H₀, H₁, φ, hH₀H₁, hH₀H₁_card⟩ := goursat H

have h_le_H₀ : Nat.card A'' ≤ Nat.card c * Nat.card H₀ := by
have h_le := Nat.card_mono (Set.toFinite _) (Set.image_subset Prod.fst hH_cover)
have h_proj_A'' : Nat.card A'' = Nat.card (Prod.fst '' A'') := Nat.card_congr
(Equiv.Set.imageOfInjOn Prod.fst A'' <|
Set.InjOn.mono (Set.Finite.subset_toFinset.mp hA') (Set.fst_injOn_graph f))
have h_proj_c : Prod.fst '' (c + H : Set (G × G')) = (Prod.fst '' c) + H₀ := by
ext x ; constructor <;> intro hx
· obtain ⟨x, ⟨⟨c, h, hc, hh, hch⟩, hx⟩⟩ := hx
rewrite [← hx]
use c.1, h.1
exact ⟨Set.mem_image_of_mem Prod.fst hc, ((hH₀H₁ h).mp hh).1, (Prod.ext_iff.mp hch).1⟩
· obtain ⟨_, h, ⟨c, hc⟩, hh, hch⟩ := hx
refine ⟨c + Prod.mk h (φ h), ⟨⟨c, Prod.mk h (φ h), ?_⟩, by rwa [← hc.2] at hch⟩⟩
exact ⟨hc.1, (hH₀H₁ ⟨h, φ h⟩).mpr ⟨hh, by rw [sub_self]; apply zero_mem⟩, rfl⟩
rewrite [← h_proj_A'', h_proj_c] at h_le
apply (h_le.trans Set.card_add_le).trans
gcongr
exact Nat.card_image_le c.toFinite

have hH₀_pos : (0 : ℝ) < Nat.card H₀ := Nat.cast_pos.mpr Nat.card_pos
have h_le_H₁ : (Nat.card H₁ : ℝ) ≤ (Nat.card c) * (Nat.card H) / Nat.card A'' := calc
_ = (Nat.card H : ℝ) / (Nat.card H₀) :=
(eq_div_iff <| ne_of_gt <| hH₀_pos).mpr <| by rw [mul_comm, ← Nat.cast_mul, hH₀H₁_card]
_ ≤ (Nat.card c : ℝ) * (Nat.card H) / Nat.card A'' := by
nth_rewrite 1 [← mul_one (Nat.card H : ℝ), mul_comm (Nat.card c : ℝ)]
repeat rewrite [mul_div_assoc]
refine mul_le_mul_of_nonneg_left ?_ (Nat.cast_nonneg _)
refine le_of_mul_le_mul_right ?_ hH₀_pos
refine le_of_mul_le_mul_right ?_ (Nat.cast_pos.mpr hA''_pos)
rewrite [div_mul_cancel 1, mul_right_comm, one_mul, div_mul_cancel, ← Nat.cast_mul]
· exact Nat.cast_le.mpr h_le_H₀
· exact ne_of_gt (Nat.cast_pos.mpr hA''_pos)
· exact ne_of_gt hH₀_pos
clear h_le_H₀ hH₀_pos hH₀H₁_card

let translate (c : G × G') (h : G') := A'' ∩ ({c} + {(0, h)} + Set.graph φ.toFun)
have h_translate (c : G × G') (h : G') :
Prod.fst '' translate c h ⊆ { x : G | f x = φ x + (-φ c.1 + c.2 + h) } := by
intro x hx
obtain ⟨x, ⟨⟨hxA'', ⟨_, x', ⟨c', h', hc, hh, hch⟩, hx, hchx⟩⟩, hxx⟩⟩ := hx
show f _ = φ _ + (-φ c.1 + c.2 + h)
replace := (Set.mem_graph x).mp <| (Set.graph f).toFinite.mem_toFinset.mp (hA' hxA'')
rewrite [← hxx, this, ← hchx, ← hch, hc, hh]
show c.2 + h + x'.2 = φ (c.1 + 0 + x'.1) + (-φ c.1 + c.2 + h)
replace : φ x'.1 = x'.2 := (Set.mem_graph x').mp hx
rw [map_add, map_add, map_zero, add_zero, this, add_comm (φ c.1), add_assoc x'.2,
← add_assoc (φ c.1), ← add_assoc (φ c.1), add_neg_self, zero_add, add_comm]
have h_translate_card c h : Nat.card (translate c h) = Nat.card (Prod.fst '' translate c h) :=
Nat.card_congr (Equiv.Set.imageOfInjOn Prod.fst (translate c h) <|
Set.InjOn.mono (fun _ hx ↦ Set.Finite.subset_toFinset.mp hA' hx.1) (Set.fst_injOn_graph f))

let cH₁ := (c ×ˢ H₁).toFinite.toFinset
replace : Nonempty c := by
haveI : Nonempty A'' := by exact Set.nonempty_coe_sort.mpr hA''_nonempty
obtain ⟨c, _, hc, _, _⟩ := hH_cover (Classical.choice this).property
exact ⟨c, hc⟩
replace h_nonempty : Set.Nonempty (c ×ˢ H₁) :=
Set.Nonempty.prod (Set.nonempty_coe_sort.mp this) (Set.nonempty_coe_sort.mp inferInstance)
replace : A' = Finset.biUnion cH₁ fun ch ↦ (translate ch.1 ch.2).toFinite.toFinset := by
ext x ; constructor <;> intro hx
· obtain ⟨c', h, hc, hh, hch⟩ := hH_cover hx
refine Finset.mem_biUnion.mpr ⟨(c', h.2 - φ h.1), ?_⟩
refine ⟨(Set.Finite.mem_toFinset _).mpr ⟨hc, ((hH₀H₁ h).mp hh).2⟩, ?_⟩
refine (Set.Finite.mem_toFinset _).mpr ⟨hx, ⟨c' + (0, h.2 - φ h.1), (h.1, φ h.1), ?_⟩⟩
refine ⟨⟨c', (0, h.2 - φ h.1), rfl, rfl, rfl⟩, ⟨⟨h.1, rfl⟩, ?_⟩⟩
beta_reduce
rewrite [add_assoc]
show c' + (0 + h.1, h.2 - φ h.1 + φ h.1) = x
rewrite [zero_add, sub_add_cancel]
exact hch
· obtain ⟨ch, hch⟩ := Finset.mem_biUnion.mp hx
exact ((Set.Finite.mem_toFinset _).mp hch.2).1

replace : ∑ __ in cH₁, ((Finset.card A) / (C₁ * (K ^ 2) ^ C₂) / cH₁.card : ℝ) ≤
∑ ch in cH₁, ((translate ch.1 ch.2).toFinite.toFinset.card : ℝ) := by
rewrite [Finset.sum_const, nsmul_eq_mul, ← mul_div_assoc, mul_div_right_comm, div_self, one_mul]
· apply hA'1.trans
norm_cast
exact (congrArg Finset.card this).trans_le Finset.card_biUnion_le
· symm
refine ne_of_lt <| Nat.cast_zero.symm.trans_lt <| Nat.cast_lt.mpr <| Finset.card_pos.mpr ?_
exact (Set.Finite.toFinset_nonempty _).mpr h_nonempty
replace : ∃ c' : G × G', ∃ h : G', (Finset.card A) / (C₁ * (K ^ 2) ^ C₂) / cH₁.card ≤
Nat.card { x : G | f x = φ x + (-φ c'.1 + c'.2 + h) } := by
obtain ⟨ch, hch⟩ :=
Finset.exists_le_of_sum_le ((Set.Finite.toFinset_nonempty _).mpr h_nonempty) this
refine ⟨ch.1, ch.2, hch.2.trans ?_⟩
rewrite [Set.Finite.card_toFinset, ← Nat.card_eq_fintype_card, h_translate_card]
exact Nat.cast_le.mpr <| Nat.card_mono (Set.toFinite _) (h_translate ch.1 ch.2)

obtain ⟨c', h, hch⟩ := this
use φ, -φ c'.1 + c'.2 + h
refine LE.le.trans ?_ hch
unfold_let cH₁
rewrite [← Nat.card_eq_finsetCard, div_div, hA]
apply div_le_div_of_le_left (Nat.cast_nonneg _) <| mul_pos h_pos1 <| Nat.cast_pos.mpr <|
Finset.card_pos.mpr <| (Set.Finite.toFinset_nonempty _).mpr h_nonempty
rewrite [← c.toFinite.toFinset_prod (H₁ : Set G').toFinite, Finset.card_product]
repeat rewrite [Set.Finite.card_toFinset, ← Nat.card_eq_fintype_card]
rewrite [Nat.cast_mul, ← mul_assoc _ (Nat.card c : ℝ)]
replace := mul_nonneg h_pos1.le (Nat.cast_nonneg (Nat.card c))
apply (mul_le_mul_of_nonneg_left h_le_H₁ this).trans
rewrite [mul_div_assoc, ← mul_assoc, mul_comm _ (Nat.card c : ℝ), mul_assoc]
have hHA := div_nonneg (α := ℝ) (Nat.cast_nonneg (Nat.card H)) <| Nat.cast_nonneg (Nat.card A'')
apply (mul_le_mul_of_nonneg_right hc_card <| mul_nonneg this hHA).trans
rewrite [mul_comm, mul_assoc, mul_comm _ (Nat.card c : ℝ), mul_assoc]
refine (mul_le_mul_of_nonneg_right hc_card ?_).trans_eq ?_
· exact mul_nonneg h_pos1.le <| mul_nonneg hHA <| by positivity
have h_pos2 : 0 < (C₃ : ℝ) * (K ^ 2) ^ C₄ :=
mul_pos (by unfold C₃; norm_num) (pow_pos (pow_pos hK 2) C₄)
haveI : Nonempty A'' := Set.nonempty_coe_sort.mpr hA''_nonempty
rewrite [mul_comm, mul_assoc, mul_assoc, mul_assoc, mul_mul_mul_comm,
← Real.rpow_add (Nat.cast_pos.mpr Nat.card_pos), mul_mul_mul_comm,
← Real.rpow_add (Nat.cast_pos.mpr Nat.card_pos), ← Real.rpow_add h_pos2]
norm_num
rewrite [mul_comm _ (Finset.card A' : ℝ), mul_assoc (Finset.card A' : ℝ),
← mul_assoc _ (Finset.card A' : ℝ), div_mul_cancel _ <|
Nat.cast_ne_zero.mpr (Finset.card_pos.mpr hA''_nonempty).ne.symm, Real.rpow_neg_one,
mul_comm (Fintype.card H : ℝ), mul_assoc _ _ (Fintype.card H : ℝ),
inv_mul_cancel <| NeZero.natCast_ne _ _, mul_one, ← pow_mul,
Real.mul_rpow (by norm_num) (pow_nonneg (sq_nonneg K) C₄), ← pow_mul,
mul_comm (K ^ _), mul_assoc _ _ (K ^ _)]
repeat rewrite [show (12 : ℝ) = ((12 : ℕ) : ℝ) from rfl]
repeat rewrite [Real.rpow_nat_cast]
rewrite [← pow_mul, ← pow_add, mul_right_comm, ← mul_assoc]
norm_num
4 changes: 4 additions & 0 deletions PFR/ForMathlib/Graph.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ namespace Set

variable {G G' : Type*}

-- TODO: maybe `Function.graph` for dot notation?
def graph (f : G → G') : Set (G×G') := {(x, f x) | x : G}

lemma graph_def (f : G → G') : graph f = {(x, f x) | x : G} := rfl
Expand All @@ -23,6 +24,9 @@ lemma mem_graph {f : G → G'} (x : G × G') : x ∈ graph f ↔ f x.1 = x.2 :=
· refine fun h ↦ ⟨x.1, ?_⟩
rw [h]

lemma fst_injOn_graph (f : G → G') : (graph f).InjOn Prod.fst := fun x hx y hy h ↦
Prod.ext h <| ((mem_graph x).mp hx).symm.trans <| (congr_arg f h).trans <| (mem_graph y).mp hy

@[simp]
lemma image_fst_graph {f : G → G'} : Prod.fst '' (graph f) = Set.univ := by
ext x; simp
Expand Down
15 changes: 8 additions & 7 deletions PFR/Main.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -153,6 +153,12 @@ theorem rdist_le_of_isUniform_of_card_add_le (h₀A : A.Nonempty) (hA : Nat.card

variable [ElementaryAddCommGroup G 2] [Fintype G]

lemma sumset_eq_sub : A + A = A - A := by
rw [← Set.image2_add, ← Set.image2_sub]
congr! 1 with a _ b _
show a + b = a - b
simp

/-- Auxiliary statement towards the polynomial Freiman-Ruzsa (PFR) conjecture: if $A$ is a subset of
an elementary abelian 2-group of doubling constant at most $K$, then there exists a subgroup $H$
such that $A$ can be covered by at most $K^{13/2} |A|^{1/2} / |H|^{1/2}$ cosets of $H$, and $H$ has
Expand All @@ -163,12 +169,7 @@ lemma PFR_conjecture_aux (h₀A : A.Nonempty) (hA : Nat.card (A + A) ≤ K * Nat
∧ Nat.card H ≤ K ^ 11 * Nat.card A ∧ Nat.card A ≤ K ^ 11 * Nat.card H ∧ A ⊆ c + H := by
classical
let _mG : MeasurableSpace G := ⊤
have hadd_sub : A + A = A - A := by
rw [<-Set.image2_add, <-Set.image2_sub]
congr! 1 with a _ b _
rw [(show a+b=a-b by simp)]
rfl
rw [hadd_sub] at hA
rw [sumset_eq_sub] at hA
have : MeasurableSingletonClass G := ⟨λ _ ↦ trivial⟩
obtain ⟨A_pos, -, K_pos⟩ : (0 : ℝ) < Nat.card A ∧ (0 : ℝ) < Nat.card (A - A) ∧ 0 < K :=
PFR_conjecture_pos_aux h₀A hA
Expand All @@ -180,7 +181,7 @@ lemma PFR_conjecture_aux (h₀A : A.Nonempty) (hA : Nat.card (A + A) ≤ K * Nat
rcases exists_isUniform_measureSpace A' h₀A' with ⟨Ω₀, mΩ₀, UA, hP₀, UAmeas, UAunif, -, -⟩
rw [hAA'] at UAunif
have : d[UA # UA] ≤ log K := rdist_le_of_isUniform_of_card_add_le h₀A hA UAunif UAmeas
rw [<-hadd_sub] at hA
rw [← sumset_eq_sub] at hA
let p : refPackage Ω₀ Ω₀ G := ⟨UA, UA, UAmeas, UAmeas, 1/9, (by norm_num), (by norm_num)⟩
-- entropic PFR gives a subgroup `H` which is close to `A` for the Rusza distance
rcases entropic_PFR_conjecture p (by norm_num) with ⟨H, Ω₁, mΩ₁, UH, hP₁, UHmeas, UHunif, hUH⟩
Expand Down
14 changes: 7 additions & 7 deletions blueprint/src/chapter/approx_hom_pfr.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,8 +28,8 @@ \chapter{Approximate homomorphism version of PFR}
Let $f: G \to G'$ be a function, and suppose that there are at least $|G|^2 / K$ pairs $(x,y) \in G^2$ such that
$$ f(x+y) = f(x) + f(y).$$
Then there exists a homomorphism $\phi: G \to G'$ and a constant $c \in G'$
such that $f(x) = \phi(x)+c$ for at least $|G| / C_1^{13} C_3^{12}
K^{24C_4+26 C_2}$ values of $x \in G$.
such that $f(x) = \phi(x)+c$ for at least $|G| / C_1 C_3^{12}
K^{24C_4 + 2C_2}$ values of $x \in G$.
\end{theorem}

\begin{proof}\uses{goursat, cs-bound, bsg, pfr_aux-improv} Consider the graph $A \subset G \times G'$ defined by
Expand All @@ -38,10 +38,10 @@ \chapter{Approximate homomorphism version of PFR}
$|A|^2/K$ pairs $(a,a') \in A^2$. By Lemma \ref{cs-bound}, this implies that
$E(A) \geq |A|^3/K^2$. Applying Lemma \ref{bsg}, we conclude that there
exists a subset $A' \subset A$ with $|A'| \geq |A|/C_1 K^{2C_2}$ and $|A'+A'|
\leq C_1C_3 K^{2(C_2+C_4)} |A'|$. Applying Lemma \ref{pfr_aux-improv}, we may
find a subspace $H \subset G \times G'$ such that $|H| / |A'| \in [L^{-10},
L^{10}$ and a subset $c$ of cardinality at most $L^6 |A'|^{1/2} / |H|^{1/2}$
such that $A' \subseteq c + H$, where $L = C_1C_3 K^{2(C_2+C_4)}$. If we let
\leq L$, where $L = C_3 K^{2C_4} |A'|$. Applying Lemma \ref{pfr_aux-improv}, we may
find a subspace $H \subset G \times G'$
and a subset $c$ of cardinality at most $L^6 |A'|^{1/2} / |H|^{1/2}$
such that $A' \subseteq c + H$. If we let
$H_0,H_1$ be as in Lemma \ref{goursat}, this implies on taking projections
the projection of $A'$ to $G$ is covered by at most $|c|$ translates of
$H_0$. This implies that
Expand All @@ -59,6 +59,6 @@ \chapter{Approximate homomorphism version of PFR}
$$

By the pigeonhole principle, one of these translates must then contain at
least $|A'|/L^{12} \geq |G| / (C_1C_3 K^{2(C_2+C_4)})^{12} (C_1 K^{2C_2})$
least $|A'|/L^{12} \geq |G| / (C_3 K^{2C_4})^{12} (C_1 K^{2C_2})$
elements of $A'$ (and hence of $A$), and the claim follows.
\end{proof}

0 comments on commit a52bc5b

Please sign in to comment.