Project-declaredLean 4.33.0-rc1 · mathlib@79d0395a1825

Better PFR conjecture

better_PFR_conjecture'

additive combinatorics entropy probability rho functional

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

Exact Lean statement

theorem better_PFR_conjecture' {G : Type*} [AddCommGroup G] [Module (ZMod 2) G]
    {A : Set G} {K : ℝ} (h₀A : A.Nonempty) (Afin : A.Finite)
    (hA : Nat.card (A + A) ≤ K * Nat.card A) :
    ∃ (H : Submodule (ZMod 2) G) (c : Set G), c.Finite ∧ (H : Set G).Finite ∧
      Nat.card c < 2 * K ^ 9 ∧ (H : Set G).ncard ≤ Nat.card A ∧ A ⊆ c + H

Formal artifact

Lean source

Canonical source

Full Lean sourceLean 4

theorem better_PFR_conjecture' {G : Type*} [AddCommGroup G] [Module (ZMod 2) G]    {A : Set G} {K : ℝ} (h₀A : A.Nonempty) (Afin : A.Finite)    (hA : Nat.card (A + A) ≤ K * Nat.card A) :    ∃ (H : Submodule (ZMod 2) G) (c : Set G), c.Finite ∧ (H : Set G).Finite ∧      Nat.card c < 2 * K ^ 9 ∧ (H : Set G).ncard ≤ Nat.card A ∧ A ⊆ c + H := by  let G' := Submodule.span (ZMod 2) A  let G'fin : Fintype G' := (Afin.submoduleSpan _).fintype  let ι : G'→ₗ[ZMod 2] G := G'.subtype  have ι_inj : Injective ι := G'.toAddSubgroup.subtype_injective  let A' : Set G' := ι ⁻¹' A  have A_rg : A ⊆ range ι := by    simp only [Submodule.coe_subtype, Subtype.range_coe_subtype, G', ι]    exact Submodule.subset_span  have cardA' : Nat.card A' = Nat.card A := Nat.card_preimage_of_injective ι_inj A_rg  have hA' : Nat.card (A' + A') ≤ K * Nat.card A' := by    rwa [cardA', ← preimage_add _ ι_inj A_rg A_rg,         Nat.card_preimage_of_injective ι_inj (add_subset_range _ A_rg A_rg)]  rcases better_PFR_conjecture (h₀A.preimage' A_rg) hA' with ⟨H', c', hc', hH', hH'₂⟩  refine ⟨H'.map ι , ι '' c', toFinite _, toFinite (ι '' H'), ?_, ?_, fun x hx ↦ ?_⟩  · rwa [Nat.card_image_of_injective ι_inj]  · simpa [Set.ncard_image_of_injective _ ι_inj, ← cardA']  · erw [← image_add]    exact ⟨⟨x, Submodule.subset_span hx⟩, hH'₂ hx, rfl⟩

Project: Polynomial Freiman-Ruzsa project
License: Apache-2.0
Commit: a177b2e4abe4
Source: PFR/RhoFunctional.lean:2134-2156

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