statement of PFR conjecture

Stream: Polynomial Freiman-Ruzsa conjecture

[Floris van Doorn]

I think this is a way to state the theorem in Lean.

import Mathlib.GroupTheory.OrderOfElement
import Mathlib.Data.Finset.Pointwise
import Mathlib.Data.Real.Basic

open Pointwise Nat

class ElementaryAddGroup (G : Type*) [AddGroup G] (p : outParam ℕ) where
  orderOf_of_ne {x : G} (hx : x ≠ 0) : addOrderOf x = p

theorem PFR_conjecture {G : Type*} [AddCommGroup G] [ElementaryAddGroup G 2] [Fintype G]
    [DecidableEq G] {A : Set G} {K : ℝ} (h₀A : A.Nonempty)
    (hA : Nat.card (A + A) ≤ K * Nat.card A) : ∃ (H : AddSubgroup G) (c : Set G),
    Nat.card c ≤ 2 * K ^ 12 ∧ Nat.card H ≤ Nat.card A ∧ A ⊆ c + H := by
  sorry

[Floris van Doorn]

Some considerations:

• This is using the formulation using elementary 2-groups instead of an explicit vector space. I think that will be nicer, if the vector space structure is not actually needed.
• Saying that A is covered by D cosets of H means that A ⊆ c + H where c is some set of cardinality at most D.
• Since we're working in a finite group, writing Set and Finset is equivalent. Not sure if the API for Nat.card is as strong as the API for Finset.card, but probably sets is nicer (note that I'm coercing H to Set in the last expression, it will be less nice to coerce it to Finset)
• Because the exponent is even, we don't even need to assume that A is nonempty or K is nonnegative :-) Oh wait, we do need that A is nonempty for |H| ≤ |A|

[Adam Topaz]

For ElementaryAddGroup wouldn't it be better to state that $n \cdot x = 0$ for all $x$? Is there a standard definition for $n$-elementary when $n$ is not prime?

[Floris van Doorn]

That is probably easier. I just wrote the statement I found on Wikipedia :-)

[Floris van Doorn]

Theorem 1.2 will look less nice, but I saw that Yael already contributed a version of Ruzsa triangle inequality to mathlib here:
file#Mathlib/Combinatorics/Additive/PluenneckeRuzsa
It is not formulated for random variables, but only for finite subsets (which presumably correspond to uniform random variables), so it might need some generalization.

[Yaël Dillies]

I'd strongly advise using Finset here. It's probably better to make AddSubgroup fit than the other way around. To be thought about...

[Bhavik Mehta]

I also strongly advise using finset - this was what Yaël and I planned when we talked about other Freiman and Ruzsa statements, and what I did for the sum-product problem which has similarities as well. The main advantage is that the Finset API is much more developed for combinatorics (partially by design because Yaël and I use it a lot for this kind of thing), see for example the statement of the Ruzsa covering lemma in mathlib

[Yaël Dillies]

Not hugely satisfying, but whenever talking about a finite subgroup, I found it workable to have s : Finset α, H : Subgroup α and hsH : (s : Set α) = H.

[Terence Tao]

By the way, we won't need too many elementary 2-groups in the argument. Besides the original group G and the eventual subgroup H, we will also work with the Cartesian square G × G... and that's about it, actually. We will need the addition homomorphism π : G × G → G := fun ⟨ x, y ⟩ ↦ x+y and the coordinate projection homomorphisms... and I think that's about it as far as group theory is concerned, aside from easy group identities such as (x+y) + (y+z) = (x+z) in a 2-group.

[Patrick Massot]

We could consider having a Finsubgroup type with the same relation to Subgroup than Finset and Set.

[Heather Macbeth]

Terence Tao said:

aside from easy group identities such as (x+y) + (y+z) = (x+z) in a 2-group.

It seems like a fun tactic-writing project would be to extend abel to know that y + y = 0 in an elementary 2-group. If anyone is looking for one ...

[Patrick Massot]

This is good opportunity to emphasize from the symmetric project that tactic writing is definitely possible and one shouldn't wait too long before asking for them. Some waiting is needed in order to understand which tactic is needed, but then maximizing pain is not a goal per se.

[Bhavik Mehta]

Heather Macbeth said:

It seems like a fun tactic-writing project would be to extend abel to know that y + y = 0 in an elementary 2-group. If anyone is looking for one ...

Similarly to simplify numerals in characteristic p using ring. I think @Eric Wieser made some progress towards this?

[David Renshaw]

reduce_mod_char was added in mathlib4#5376

[Bhavik Mehta]

Oh amazing, thanks for the heads-up!

[Yaël Dillies]

Patrick Massot said:

We could consider having a Finsubgroup type with the same relation to Subgroup than Finset and Set.

Yeah, that would be quite an improvement! But of course we don't want to need duplicating too much API. On the other, people do care about the collection of finite subgroups sometimes, no?

[Oliver Nash]

If we do create Finsubgroup I'd like to advocate for it be a non-constructive Prop-only extension of Subgroup.