Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: Improve other bounds using PFR 9 #232

Merged
merged 4 commits into from
Nov 19, 2024
Merged

feat: Improve other bounds using PFR 9 #232

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
d3685a1
improve
sgouezel Nov 18, 2024
6c7c8eb
actualize blueprint
sgouezel Nov 18, 2024
376f975
fix examples file
sgouezel Nov 19, 2024
5dba0b8
space
sgouezel Nov 19, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Next Next commit
improve
  • Loading branch information
@sgouezel
sgouezel committed Nov 18, 2024
commit d3685a1bd7511f9af8044f6d967f5f471d141861
15 changes: 8 additions & 7 deletions PFR/ApproxHomPFR.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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]
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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]
Expand All @@ -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
13 changes: 7 additions & 6 deletions PFR/HomPFR.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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⟩
Expand Down
15 changes: 13 additions & 2 deletions examples.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
import PFR.ApproxHomPFR
import PFR.ImprovedPFR
import PFR.WeakPFR
import PFR.RhoFunctional

section PFR

Expand All @@ -12,7 +13,7 @@ variable {G' : Type*} [AddCommGroup G'] [Module (ZMod 2) G'] [Fintype G']

/-- A self-contained version of the PFR conjecture using only Mathlib definitions. -/
example {A : Set G} {K : ℝ} (h₀A : A.Nonempty) (hA : Nat.card (A + A) ≤ K * Nat.card A) :
∃ (H : AddSubgroup G) (c : Set G),
∃ (H : Submodule (ZMod 2) G) (c : Set G),
Nat.card c < 2 * K ^ 12 ∧ Nat.card H ≤ Nat.card A ∧ A ⊆ c + H := by
convert PFR_conjecture h₀A hA
norm_cast
Expand All @@ -21,13 +22,23 @@ example {A : Set G} {K : ℝ} (h₀A : A.Nonempty) (hA : Nat.card (A + A) ≤ K

/-- The improved version -/
example {A : Set G} {K : ℝ} (h₀A : A.Nonempty) (hA : Nat.card (A + A) ≤ K * Nat.card A) :
∃ (H : AddSubgroup G) (c : Set G),
∃ (H : Submodule (ZMod 2) G) (c : Set G),
Nat.card c < 2 * K ^ 11 ∧ Nat.card H ≤ Nat.card A ∧ A ⊆ c + H := by
convert PFR_conjecture_improv h₀A hA
norm_cast

#print axioms PFR_conjecture_improv

/-- The even more improved version -/
example {A : Set G} {K : ℝ} (h₀A : A.Nonempty) (hA : Nat.card (A + A) ≤ K * Nat.card A) :
∃ (H : Submodule (ZMod 2) G) (c : Set G),
Nat.card c < 2 * K ^ 9 ∧ Nat.card H ≤ Nat.card A ∧ A ⊆ c + H := by
convert better_PFR_conjecture h₀A hA
norm_cast

#print axioms better_PFR_conjecture

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

By the way, this examples file is very much broken. I guess it isn't tested by CI, and I'm not sure what its role is.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it is referenced on Terry's blog? It should very much be checked by CI!


/-- The homomorphism version of PFR. -/
example (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, f x - φ x ∈ T := homomorphism_pfr f S hS
Expand Down