teorth · YaelDillies · Nov 19, 2024 · Nov 18, 2024 · Nov 18, 2024 · Nov 19, 2024
diff --git a/PFR/ApproxHomPFR.lean b/PFR/ApproxHomPFR.lean
@@ -3,6 +3,7 @@ import Mathlib.Analysis.Normed.Lp.PiLp
 import Mathlib.Analysis.InnerProductSpace.PiL2
 import LeanAPAP.Extras.BSG
 import PFR.HomPFR
+import PFR.RhoFunctional
 
 /-!
 # The approximate homomorphism form of PFR
@@ -28,10 +29,10 @@ variable {G G' : Type*} [AddCommGroup G] [Fintype G] [AddCommGroup G'] [Fintype
 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| / (2 ^ {172} * K ^ {146})$ values of $x \in G$. -/
+$f(x) = \phi(x)+c$ for at least $|G| / (2 ^ {144} * K ^ {122})$ values of $x \in G$. -/
 theorem approx_hom_pfr (f : G → G') (K : ℝ) (hK : K > 0)
     (hf : Nat.card G ^ 2 / K ≤ Nat.card {x : G × G | f (x.1 + x.2) = f x.1 + f x.2}) :
-    ∃ (φ : G →+ G') (c : G'), Nat.card {x | f x = φ x + c} ≥ Nat.card G / (2 ^ 172 * K ^ 146) := by
+    ∃ (φ : G →+ G') (c : G'), Nat.card {x | f x = φ x + c} ≥ Nat.card G / (2 ^ 144 * K ^ 122) := by
   let A := (Set.univ.graphOn f).toFinite.toFinset
   have hA : #A = Nat.card G := by rw [Set.Finite.card_toFinset]; simp [← Nat.card_eq_fintype_card]
   have hA_nonempty : A.Nonempty := by simp [-Set.Finite.toFinset_setOf, A]
@@ -64,7 +65,7 @@ theorem approx_hom_pfr (f : G → G') (K : ℝ) (hK : K > 0)
   replace : Nat.card (A'' + A'') ≤ 2 ^ 14 * K ^ 12 * Nat.card A'' := by
     rewrite [← this, hA''_coe]
     simpa [← pow_mul] using hA'2
-  obtain ⟨H, c, hc_card, hH_le, hH_ge, hH_cover⟩ := PFR_conjecture_improv_aux hA''_nonempty this
+  obtain ⟨H, c, hc_card, hH_le, hH_ge, hH_cover⟩ := better_PFR_conjecture_aux hA''_nonempty this
   clear hA'2 hA''_coe hH_le hH_ge
   obtain ⟨H₀, H₁, φ, hH₀H₁, hH₀H₁_card⟩ := goursat H
 
@@ -168,7 +169,7 @@ theorem approx_hom_pfr (f : G → G') (K : ℝ) (hK : K > 0)
     · positivity
     · rewrite [Nat.cast_pos, Finset.card_pos, Set.Finite.toFinset_nonempty _]
       exact h_nonempty
-  rw [show 146 = 2 + 144 by norm_num, show 172 = 4 + 168 by norm_num, pow_add, pow_add,
+  rw [show 122 = 2 + 120 by norm_num, show 144 = 4 + 140 by norm_num, pow_add, pow_add,
     mul_mul_mul_comm]
   gcongr
   rewrite [← c.toFinite.toFinset_prod (H₁ : Set G').toFinite, Finset.card_product]
@@ -178,17 +179,17 @@ theorem approx_hom_pfr (f : G → G') (K : ℝ) (hK : K > 0)
   refine (mul_le_mul_of_nonneg_right hc_card (by positivity)).trans ?_
   rewrite [mul_div_left_comm, mul_assoc]
   refine (mul_le_mul_of_nonneg_right hc_card (by positivity)).trans_eq ?_
-  rw [mul_assoc ((_ * _)^6), mul_mul_mul_comm, mul_comm (_ ^ (1/2) * _), mul_comm_div,
+  rw [mul_assoc ((_ * _)^5), mul_mul_mul_comm, mul_comm (_ ^ (1/2) * _), mul_comm_div,
     ← mul_assoc _ (_^_) (_^_), mul_div_assoc, mul_mul_mul_comm _ (_^_) (_^_),
     ← mul_div_assoc, mul_assoc _ (_^(1/2)) (_^(1/2)),
     ← Real.rpow_add (Nat.cast_pos.mpr Nat.card_pos), add_halves, Real.rpow_one,
     ← Real.rpow_add (Nat.cast_pos.mpr Nat.card_pos), add_halves, Real.rpow_neg_one,
-    mul_comm _ (_ / _), mul_assoc (_^6)]
+    mul_comm _ (_ / _), mul_assoc (_^5)]
   conv => { lhs; rhs; rw [← mul_assoc, ← mul_div_assoc, mul_comm_div, mul_div_assoc] }
   rw [div_self <| Nat.cast_ne_zero.mpr (Nat.ne_of_lt Nat.card_pos).symm, mul_one]
   rw [mul_inv_cancel₀ <| Nat.cast_ne_zero.mpr (Nat.ne_of_lt Nat.card_pos).symm, one_mul, ← sq,
     ← Real.rpow_two, ← Real.rpow_mul (by positivity), Real.mul_rpow (by positivity) (by positivity)]
   have : K ^ (12 : ℕ) = K ^ (12 : ℝ) := (Real.rpow_natCast K 12).symm
   rw [this, ← Real.rpow_mul (by positivity)]
   norm_num
-  exact Real.rpow_natCast K 144
+  exact Real.rpow_natCast K 120
diff --git a/PFR/HomPFR.lean b/PFR/HomPFR.lean
@@ -2,6 +2,7 @@ import Mathlib.Data.Set.Card
 import PFR.Mathlib.LinearAlgebra.Basis.VectorSpace
 import PFR.Mathlib.SetTheory.Cardinal.Finite
 import PFR.ImprovedPFR
+import PFR.RhoFunctional
 
 /-!
 # The homomorphism form of PFR
@@ -16,7 +17,7 @@ few values.
   abelian 2-groups.
 * `homomorphism_pfr` : If $f : G → G'$ is a map between finite abelian elementary 2-groups such
   that $f(x+y)-f(x)-f(y)$ takes at most $K$ values, then there is a homomorphism $\phi: G \to G'$
-  such that $f(x)-\phi(x)$ takes at most $K^{12}$ values.
+  such that $f(x)-\phi(x)$ takes at most $K^{10}$ values.
 -/
 
 open Set
@@ -64,9 +65,9 @@ open Set Fintype
 /-- Let $f: G \to G'$ be a function, and let $S$ denote the set
 $$ S := \{ f(x+y)-f(x)-f(y): x,y \in G \}.$$
 Then there exists a homomorphism $\phi: G \to G'$ such that
-$$ |\{f(x) - \phi(x)\}| \leq |S|^{12}. $$ -/
+$$ |\{f(x) - \phi(x)\}| \leq |S|^{10}. $$ -/
 theorem homomorphism_pfr (f : G → G') (S : Set G') (hS : ∀ x y : G, f (x+y) - (f x) - (f y) ∈ S) :
-  ∃ (φ : G →+ G') (T : Set G'), Nat.card T ≤ Nat.card S ^ 12 ∧ ∀ x : G, (f x) - (φ x) ∈ T := by
+  ∃ (φ : G →+ G') (T : Set G'), Nat.card T ≤ Nat.card S ^ 10 ∧ ∀ x : G, (f x) - (φ x) ∈ T := by
   classical
   have : 0 < Nat.card G := Nat.card_pos
   let A := univ.graphOn f
@@ -88,7 +89,7 @@ theorem homomorphism_pfr (f : G → G') (S : Set G') (hS : ∀ x y : G, f (x+y)
     norm_cast
     exact (Nat.card_mono (toFinite B) hAB).trans hB_card
   have hA_nonempty : A.Nonempty := by simp [A]
-  obtain ⟨H, c, hcS, -, -, hAcH⟩ := PFR_conjecture_improv_aux hA_nonempty hA_le
+  obtain ⟨H, c, hcS, -, -, hAcH⟩ := better_PFR_conjecture_aux hA_nonempty hA_le
   have : 0 < Nat.card c := by
     have : c.Nonempty := by
       by_contra! H
@@ -139,7 +140,7 @@ theorem homomorphism_pfr (f : G → G') (S : Set G') (hS : ∀ x y : G, f (x+y)
         congr! 3 with a
         rw [← range, ← range, ← graphOn_univ_eq_range, ← graphOn_univ_eq_range, vadd_graphOn_univ]
   refine ⟨φ, T, ?_, ?_⟩
-  · have : (Nat.card T : ℝ) ≤ (Nat.card S : ℝ) ^ (12 : ℝ) := by calc
+  · have : (Nat.card T : ℝ) ≤ (Nat.card S : ℝ) ^ (10 : ℝ) := by calc
       (Nat.card T : ℝ) ≤ Nat.card (c + {(0 : G)} ×ˢ (H₁ : Set G')) := by
         norm_cast; apply Nat.card_image_le (toFinite _)
       _ ≤ Nat.card c * Nat.card H₁ := by
@@ -148,9 +149,9 @@ theorem homomorphism_pfr (f : G → G') (S : Set G') (hS : ∀ x y : G, f (x+y)
         rw [Set.card_singleton_prod] ; rfl
       _ ≤ Nat.card c * ((Nat.card H / Nat.card A) * Nat.card c) := by gcongr
       _ = Nat.card c ^ 2 * (Nat.card H / Nat.card A) := by ring
-      _ ≤ (Nat.card S ^ (6 : ℝ) * Nat.card A ^ (1 / 2 : ℝ) * Nat.card H ^ (-1 / 2 : ℝ)) ^ 2
+      _ ≤ (Nat.card S ^ (5 : ℝ) * Nat.card A ^ (1 / 2 : ℝ) * Nat.card H ^ (-1 / 2 : ℝ)) ^ 2
           * (Nat.card H / Nat.card A) := by gcongr
-      _ = (Nat.card S : ℝ) ^ (12 : ℝ) := by
+      _ = (Nat.card S : ℝ) ^ (10 : ℝ) := by
         rw [← Real.rpow_two, div_eq_mul_inv, div_eq_mul_inv, div_eq_mul_inv]
         have : 0 < Nat.card S := by
           have : S.Nonempty := ⟨f (0 + 0) - f 0 - f 0, hS 0 0⟩

diff --git a/PFR/Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean b/PFR/Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean
@@ -0,0 +1,21 @@
+import Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
+import PFR.Mathlib.SetTheory.Cardinal.Arithmetic
+
+open Cardinal Module Module Set Submodule
+
+universe u v
+
+variable {K : Type u} {V : Type v} [Ring K] [StrongRankCondition K]
+  [AddCommGroup V] [Module K V] [Module.Free K V] [Module.Finite K V]
+
+variable (K V) in
+theorem cardinal_le_aleph0_of_finiteDimensional [h : Countable K] :
+    #V ≤ ℵ₀ := by
+  rw [← lift_le_aleph0.{v, u}, lift_cardinal_mk_eq_lift_cardinal_mk_field_pow_lift_rank K V]
+  apply power_le_aleph0 (lift_le_aleph0.mpr (mk_le_aleph0_iff.mpr h))
+    (lift_lt_aleph0.mpr (rank_lt_aleph0 K V))
+
+variable (K V) in
+theorem countable_of_finiteDimensional [h : Countable K] : Countable V := by
+  have : #V ≤ ℵ₀ := cardinal_le_aleph0_of_finiteDimensional K V
+  exact mk_le_aleph0_iff.mp this
diff --git a/PFR/Mathlib/SetTheory/Cardinal/Arithmetic.lean b/PFR/Mathlib/SetTheory/Cardinal/Arithmetic.lean
@@ -0,0 +1,14 @@
+import Mathlib.SetTheory.Cardinal.Arithmetic
+
+universe u
+
+open Function Set Cardinal Equiv Order Ordinal
+
+
+/- Put just after `power_nat_eq` -/
+theorem power_le_aleph0 {a b : Cardinal.{u}} (ha : a ≤ ℵ₀) (hb : b < ℵ₀) : a ^ b ≤ ℵ₀ := by
+  rcases lt_aleph0.1 hb with ⟨n, rfl⟩
+  have : a ^ (n : Cardinal.{u}) ≤ ℵ₀ ^ (n : Cardinal.{u}) := power_le_power_right ha
+  apply this.trans
+  simp only [power_natCast]
+  exact power_nat_le le_rfl
diff --git a/PFR/WeakPFR.lean b/PFR/WeakPFR.lean
@@ -1,6 +1,8 @@
+import Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
 import Mathlib.LinearAlgebra.FreeModule.PID
 import Mathlib.MeasureTheory.Constructions.SubmoduleQuotient
 import PFR.Mathlib.Data.Set.Pointwise.SMul
+import PFR.Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
 import PFR.ForMathlib.AffineSpaceDim
 import PFR.ForMathlib.Entropy.RuzsaSetDist
 import PFR.ForMathlib.GroupQuot
@@ -599,10 +601,10 @@ variable [Module.Finite ℤ G]
 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 -/
 lemma third_iso {G : Type*} [AddCommGroup G] {G₂ : AddSubgroup G} (H' : AddSubgroup (G ⧸ G₂)) :
-  let H := G ⧸ G₂
-  let φ : G →+ H := mk' G₂
-  let N := AddSubgroup.comap φ H'
-  ∃ e : H ⧸ H' ≃+ G ⧸ N, ∀ x : G, e (mk' H' (φ x))= mk' N x := by
+    let H := G ⧸ G₂
+    let φ : G →+ H := mk' G₂
+    let N := AddSubgroup.comap φ H'
+    ∃ e : H ⧸ H' ≃+ G ⧸ N, ∀ x : G, e (mk' H' (φ x)) = mk' N x := by
   set H := G ⧸ G₂
   let φ : G →+ H := mk' G₂
   let N := AddSubgroup.comap φ H'
@@ -624,7 +626,7 @@ lemma third_iso {G : Type*} [AddCommGroup G] {G₂ : AddSubgroup G} (H' : AddSub
   convert (quotientQuotientEquivQuotientAux_mk_mk _ _ h1 x) using 1
 
 lemma single {Ω : Type*} [MeasurableSpace Ω] [DiscreteMeasurableSpace Ω] (μ : Measure Ω)
-    [IsProbabilityMeasure μ] {A : Set Ω} {z : Ω} (hA : μ.real A = 1) (hz : μ.real {z} > 0) :
+    [IsProbabilityMeasure μ] {A : Set Ω} {z : Ω} (hA : μ.real A = 1) (hz : 0 < μ.real {z}) :
     z ∈ A := by
   contrapose! hz
   have : Disjoint {z} A := by simp [hz]
@@ -1087,16 +1089,24 @@ lemma weak_PFR {A : Set G} [Finite A] {K : ℝ} (hA : A.Nonempty) (hK : 0 < 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$.-/
-theorem weak_PFR_int {A : Set G} [A_fin : Finite A] (hnA : A.Nonempty) {K : ℝ} (hK : 0 < K)
+theorem weak_PFR_int
+    {G : Type*} [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' : Set G, A' ⊆ A ∧ Nat.card A' ≥ K ^ (-17 : ℝ) * Nat.card A ∧
       AffineSpace.finrank ℤ A' ≤ (40 / log 2) * log K := by
+  have : Nonempty (A - A) := (hnA.sub hnA).coe_sort
+  have : Finite (A - A) := Set.Finite.sub A_fin A_fin
+  have hK : 0 < K := by
+    have : 0 < K * Nat.card A := lt_of_lt_of_le (mod_cast Nat.card_pos) hA
+    have : (0 : ℝ) ≤ Nat.card A := Nat.cast_nonneg' _
+    nlinarith
+  have : Countable G := countable_of_finiteDimensional ℤ G
+  let m : MeasurableSpace G := ⊤
   apply weak_PFR hnA hK ((rdist_set_le A A hnA hnA).trans _)
   suffices log (Nat.card (A-A)) ≤ log K + log (Nat.card A) by linarith
   rw [← log_mul (by positivity) _]
   · apply log_le_log _ hA
     norm_cast
-    have : Nonempty (A - A) := (hnA.sub hnA).coe_sort
-    have : Finite (A - A) := Set.Finite.sub A_fin A_fin
     exact Nat.card_pos
   exact_mod_cast ne_of_gt (@Nat.card_pos _ hnA.to_subtype _)
diff --git a/blueprint/src/chapter/approx_hom_pfr.tex b/blueprint/src/chapter/approx_hom_pfr.tex
@@ -28,22 +28,23 @@ \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| / (2 ^ {172} * K ^ {146})$ values of $x \in G$.
+such that $f(x) = \phi(x)+c$ for at least $|G| / (2 ^ {144} * K ^ {122})$
+values of $x \in G$.
 \end{theorem}
 
 \begin{proof}\uses{goursat, cs-bound, bsg, pfr_aux-improv}\leanok Consider the graph $A \subset G \times G'$ defined by
 $$ A := \{ (x,f(x)): x \in G \}.$$
 Clearly, $|A| = |G|$.  By hypothesis, we have $a+a' \in A$ for at least
-$|A|^2/K$ pairs $(a,a') \in A^2$. By \Cref{cs-bound}, this implies that
-$E(A) \geq |A|^3/K^2$.  Applying \Cref{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 \Cref{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
-$H_0,H_1$ be as in \Cref{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
+$|A|^2/K$ pairs $(a,a') \in A^2$. By \Cref{cs-bound}, this implies that $E(A)
+\geq |A|^3/K^2$.  Applying \Cref{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 \Cref{pfr-9-aux'}, we may find a subspace $H
+\subset G \times G'$ such that $|H| / |A'| \in [L^{-8}, L^{8}]$ and a subset
+$c$ of cardinality at most $L^5 |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 $H_0,H_1$ be
+as in \Cref{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
 $$ |c| |H_0| \geq |A'|;$$
 since $|H_0| |H_1| = |H|$, we conclude that
 $$ |H_1| \leq |c| |H|/|A'|.$$
@@ -54,10 +55,10 @@ \chapter{Approximate homomorphism version of PFR}
 (x,\phi(x)+c): x \in G \}$ for some $c \in G'$. The number of translates is
 bounded by
 $$
-|c|^2 \frac{|H|}{|A'|} \leq \left(L^6 \frac{|A'|^{1/2}}{|H|^{1/2}}\right)^2 \frac{|H|}{|A'|} = L^{12}.
+|c|^2 \frac{|H|}{|A'|} \leq \left(L^5 \frac{|A'|^{1/2}}{|H|^{1/2}}\right)^2 \frac{|H|}{|A'|} = L^{10}.
 $$
 
 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^{10} \geq |G| / (C_1C_3 K^{2(C_2+C_4)})^{10} (C_1 K^{2C_2})$
 elements of $A'$ (and hence of $A$), and the claim follows.
 \end{proof}
diff --git a/blueprint/src/chapter/further_improvement.tex b/blueprint/src/chapter/further_improvement.tex
@@ -344,19 +344,34 @@ \section{Studying a minimizer}
 By \Cref{rho-invariant} we get $\rho(U_{H_1})+\rho(U_{H_2})\le \rho(Y_1) + \rho(Y_2) + 8 d[Y_1;Y_2]$, and thus the claim holds for $H=H_1$ or $H=H_2$.
 \end{proof}
 
-\begin{corollary}\label{pfr-9-aux}\lean{better_PFR_conjecture_aux}\leanok
-If $|A+A| \leq K|A|$, then there exists a subgroup $H$ and $t\in G$ such that $|A \cap (H+t)| \geq K^{-4} \sqrt{|A||V|}$, and $|H|/|A|\in[K^{-8},K^8]$.
+\begin{corollary}\label{pfr-9-aux}\lean{better_PFR_conjecture_aux0}\leanok
+If $|A+A| \leq K|A|$, then there exists a subgroup $H$ and $t\in G$ such that
+$|A \cap (H+t)| \geq K^{-4} \sqrt{|A||H|}$, and $|H|/|A|\in[K^{-8},K^8]$.
 \end{corollary}
 
 \begin{proof}\leanok
   \uses{pfr-rho,rho-init,rho-subgroup}
   Apply \Cref{pfr-rho} on $U_A,U_A$ to get a subspace such that $2\rho(U_H)\le 2\rho(U_A)+8d[U_A;U_A]$. Recall that $d[U_A;U_A]\le \log K$ as proved in \Cref{pfr_aux}, and $\rho(U_A)=0$ by \Cref{rho-init}. Therefore $\rho(U_H)\le 4\log(K)$. The claim then follows from \Cref{rho-subgroup}.
 \end{proof}
 
+
+\begin{corollary}\label{pfr-9-aux'}\lean{better_PFR_conjecture_aux}\leanok
+If $|A+A| \leq K|A|$, then there exist a subgroup $H$ and a subset $c$ of $G$
+with $A \subseteq c + H$, such that $|c| \leq K^{5} |A|^{1/2}/|H|^{1/2}$ and
+$|H|/|A|\in[K^{-8},K^8]$.
+\end{corollary}
+
+\begin{proof}\leanok
+  \uses{pfr-9-aux, ruz-cov}
+Apply \Cref{pfr-9-aux} and \Cref{ruz-cov} to get the result, as in the proof
+of \Cref{pfr_aux}.
+\end{proof}
+
+
 \begin{theorem}[PFR with \texorpdfstring{$C=9$}{C=9}]\label{pfr-9}\lean{better_PFR_conjecture}\leanok  If $A \subset {\bf F}_2^n$ is finite non-empty with $|A+A| \leq K|A|$, then there exists a subgroup $H$ of ${\bf F}_2^n$ with $|H| \leq |A|$ such that $A$ can be covered by at most $2K^9$ translates of $H$.
 \end{theorem}
 
 \begin{proof}\leanok
   \uses{pfr-9-aux,ruz-cov}
-Apply \Cref{pfr-9-aux} and \Cref{ruz-cov} to get a variant of \Cref{pfr_aux}. The remaining part is the same as \Cref{pfr}.
+Given \Cref{pfr-9-aux'}, the proof is the same as that of \Cref{pfr}.
 \end{proof}
diff --git a/blueprint/src/chapter/hom_pfr.tex b/blueprint/src/chapter/hom_pfr.tex
@@ -19,20 +19,19 @@ \chapter{Homomorphism version of PFR}
 \begin{theorem}[Homomorphism form of PFR]\label{hom-pfr}\lean{homomorphism_pfr}\leanok  Let $f: G \to G'$ be a function, and let $S$ denote the set
 $$ S := \{ f(x+y)-f(x)-f(y): x,y \in G \}.$$
 Then there exists a homomorphism $\phi: G \to G'$ such that
-$$ |\{ f(x) - \phi(x): x \in G \}| \leq |S|^{12}.$$
+$$ |\{ f(x) - \phi(x): x \in G \}| \leq |S|^{10}.$$
 \end{theorem}
 
 \begin{proof}\uses{goursat, pfr_aux-improv}\leanok
 Consider the graph $A \subset G \times G'$ defined by
 $$ A := \{ (x,f(x)): x \in G \}.$$
 Clearly, $|A| = |G|$.  By hypothesis, we have
 $$ A+A \subset \{ (x,f(x)+s): x \in G, s \in S\}$$
-and hence $|A+A| \leq |S| |A|$.  Applying \Cref{pfr_aux-improv}, we may
-find a subspace $H \subset G \times G'$ such that $|H|/ |A| \in [K^{-10},
-K^{10}]$ and $A$ is covered by $c + H$ with $|c| \le |S|^6|A|^{1/2} /
-|H|^{1/2}$. If we let $H_0, H_1$ be as in \Cref{goursat}, this implies
-on taking projections that $G$ is covered by at most $|c|$ translates of
-$H_0$. This implies that
+and hence $|A+A| \leq |S| |A|$.  Applying \Cref{pfr-9-aux'}, we may find a
+subspace $H \subset G \times G'$ such that $|H|/ |A| \in [|S|^{-8}, |S|^{8}]$
+and $A$ is covered by $c + H$ with $|c| \le |S|^5|A|^{1/2} / |H|^{1/2}$. If
+we let $H_0, H_1$ be as in \Cref{goursat}, this implies on taking projections
+that $G$ is covered by at most $|c|$ translates of $H_0$. This implies that
 $$ |c| |H_0| \geq |G|;$$
 since $|H_0| |H_1| = |H|$, we conclude that
 $$ |H_1| \leq |c| |H|/|G| = |c| |H|/|A|.$$
@@ -41,8 +40,8 @@ \chapter{Homomorphism version of PFR}
 is a homomorphism, each such translate can be written in the form $\{
 (x,\phi(x)+d): x \in G \}$ for some $d \in G'$. Since
 $$
-|c| |H_1| \le |c|^2 \frac{|H|}{|A|} \le \left(|S|^6 \frac{|A|^{1/2}}{|H|^{1/2}}\right)^2 \frac{|H|}{|A|}
-= |S|^{12},
+|c| |H_1| \le |c|^2 \frac{|H|}{|A|} \le \left(|S|^5 \frac{|A|^{1/2}}{|H|^{1/2}}\right)^2 \frac{|H|}{|A|}
+= |S|^{10},
 $$
 the result follows.
 \end{proof}