Project-declaredLean 4.33.0-rc1 · mathlib@79d0395a1825

PFR conjecture

PFR_conjecture

additive combinatorics entropy probability main

Plain-language statement

The polynomial Freiman-Ruzsa (PFR) conjecture: if A is a subset of an elementary abelian 2-group of doubling constant at most K, then A can be covered by at most 2 * K ^ 12 cosets of a subgroup of cardinality at most |A|.

Exact Lean statement

theorem PFR_conjecture (hA₀ : A.Nonempty) (hA : (A + A).ncard ≤ K * A.ncard) :
     ∃ (H : Submodule (ZMod 2) G) (c : Set G),
      Nat.card c < 2 * K ^ 12 ∧ (H : Set G).ncard ≤ A.ncard ∧ A ⊆ c + H

Formal artifact

Lean source

Canonical source

Full Lean sourceLean 4

theorem PFR_conjecture (hA₀ : A.Nonempty) (hA : (A + A).ncard ≤ K * A.ncard) :     ∃ (H : Submodule (ZMod 2) G) (c : Set G),      Nat.card c < 2 * K ^ 12 ∧ (H : Set G).ncard ≤ A.ncard ∧ A ⊆ c + H := by  obtain ⟨A_pos, -, K_pos⟩ : (0 : ℝ) < A.ncard ∧ (0 : ℝ) < (A + A).ncard ∧ 0 < K :=    PFR_conjecture_pos_aux' A.toFinite hA₀ hA  -- consider the subgroup `H` given by Lemma `PFR_conjecture_aux`.  obtain ⟨H, c, hc, IHA, IAH, A_subs_cH⟩ : ∃ (H : Submodule (ZMod 2) G) (c : Set G),    Nat.card c ≤ K ^ (13/2) * A.ncard ^ (1/2) * (H : Set G).ncard ^ (-1/2)      ∧ (H : Set G).ncard ≤ K ^ 11 * A.ncard ∧ A.ncard ≤ K ^ 11 * (H : Set G).ncard      ∧ A ⊆ c + H :=    PFR_conjecture_aux hA₀ hA  have H_pos : (0 : ℝ) < (H : Set G).ncard := by    have : 0 < (H : Set G).ncard := Nat.card_pos; positivity  rcases le_or_gt ((H : Set G).ncard) A.ncard with h|h  -- If `#H ≤ #A`, then `H` satisfies the conclusion of the theorem  · refine ⟨H, c, ?_, h, A_subs_cH⟩    calc    Nat.card c ≤ K ^ (13/2 : ℝ) * A.ncard ^ (1/2 : ℝ) * (H : Set G).ncard ^ (-1/2 : ℝ) := hc    _ ≤ K ^ (13/2 : ℝ) * (K ^ 11 * (H : Set G).ncard) ^ (1/2) * (H : Set G).ncard ^ (-1/2 : ℝ) := by      gcongr    _ = K ^ 12 := by rpow_ring; norm_num    _ < 2 * K ^ 12 := by linarith [show 0 < K ^ 12 by positivity]  -- otherwise, we decompose `H` into cosets of one of its subgroups `H'`, chosen so that  -- `#A / 2 < #H' ≤ #A`. This `H'` satisfies the desired conclusion.  · obtain ⟨H', IH'A, IAH', H'H⟩ : ∃ H' : Submodule (ZMod 2) G, Nat.card H' ≤ A.ncard          ∧ A.ncard < 2 * Nat.card H' ∧ H' ≤ H := by      have A_pos' : 0 < A.ncard := mod_cast A_pos      exact ZModModule.exists_submodule_subset_card_le Nat.prime_two H h.le A_pos'.ne'    have : (A.ncard / 2 : ℝ) < Nat.card H' := by      rw [div_lt_iff₀ zero_lt_two, mul_comm]; norm_cast    have H'_pos : (0 : ℝ) < Nat.card H' := by      have : 0 < Nat.card H' := Nat.card_pos; positivity    obtain ⟨u, HH'u, hu⟩ :=      H'.toAddSubgroup.exists_left_transversal_of_le (H := H.toAddSubgroup) H'H    dsimp at HH'u    refine ⟨H', c + u, ?_, IH'A, by rwa [add_assoc, HH'u]⟩    calc    (Nat.card (c + u) : ℝ)      ≤ Nat.card c * Nat.card u := mod_cast natCard_add_le    _ ≤ (K ^ (13/2 : ℝ) * A.ncard ^ (1 / 2 : ℝ) * ((H : Set G).ncard ^ (-1 / 2 : ℝ)))          * ((H : Set G).ncard / Nat.card H') := by        gcongr        apply le_of_eq        rw [eq_div_iff H'_pos.ne']        norm_cast    _ < (K ^ (13/2) * A.ncard ^ (1 / 2) * ((H : Set G).ncard ^ (-1 / 2)))          * ((H : Set G).ncard / (A.ncard / 2)) := by        gcongr    _ = 2 * K ^ (13/2) * A.ncard ^ (-1/2) * (H : Set G).ncard ^ (1/2) := by        field_simp        rpow_ring        norm_num    _ ≤ 2 * K ^ (13/2) * A.ncard ^ (-1/2) * (K ^ 11 * A.ncard) ^ (1/2) := by        gcongr    _ = 2 * K ^ 12 := by        rpow_ring        norm_num

Project: Polynomial Freiman-Ruzsa project
License: Apache-2.0
Commit: a177b2e4abe4
Source: PFR/Main.lean:253-309

Reuse this declaration

Bring the exact result into your workflow

The import identifies the source module. Your project still needs the pinned package dependency shown on this page.

What this badge means

This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.

Continue in this project

Related declarations

Project-declaredLean 4.33.0-rc1

Approx hom pfr

approx_hom_pfr

Project documentation

An approximate-homomorphism theorem for finite elementary abelian $2$ -groups. Let $f:G\to G'$ and $K>0$ . If at least a proportion $K^{-1}$ of pairs $(x,y)\in G^2$ satisfy $f(x+y)=f(x)+f(y)$ , then there are an additive homomorphism $\varphi:G\to G'$ and a constant $c\in G'$ such that $f(x)=\varphi(x)+c$ for at least $|G|/(2^{144}K^{122})$ values of $x$ .

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record

Project-declaredLean 4.33.0-rc1

Better PFR conjecture

better_PFR_conjecture

Plain-language statement

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$ .

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record

Project-declaredLean 4.33.0-rc1

Better PFR conjecture

better_PFR_conjecture'

Project documentation

Polynomial Freiman-Ruzsa theorem with exponent $9$ , without a finite ambient-group assumption. Let $A$ be a nonempty finite subset of an elementary abelian $2$ -group. If $|A+A|\le K|A|$ , then there are a finite subspace $H$ and a finite set $c$ such that $A\subseteq c+H$ , $|c|<2K^9$ , and $|H|\le|A|$ .

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record