Mismatch between BSG in survey and LeanAPAP

Stream: maths

[Daniel Weber]

I'm trying to formalize Bourgain's randomness extractor, following Incidence Theorems and Their Applications, Zeev Dvir. I have noticed that LeanAPAP has the BSG theorem (note that E[A,B] there is $|Q(a,b)|$ in the survey, and the survey's $E(a,b)$ is A.card^2 * B.card^2 / E[A,B]), but the statements of the theorem seem different—in theorem 3.3.2 there are two subsets with a small sum, while in LeanAPAP there is only a single subset which doesn't grow much.
Are these two statements equivalent by some argument I'm not seeing? Are there two versions of BSG?

[Yaël Dillies]

Indeed there are many variants of BSG. Let me try to match up your statement and mine

[Yaël Dillies]

(btw it would be nice if LeanAPAP#BSG could be linkified)

[Yaël Dillies]

I must say Theorem 3.3.2 is a weird statement. It forces A and B to have the same size. From BSG in LeanAPAP you can deduce that there are some A' ⊆ A, B' ⊆ B such that |A' - A'| and |B' - B'| are small, but I don't currently see how to get |A' + B'| small from it

[Thomas Bloom]

Yes, there are a few basically equivalent versions around. The version with two different sets (of the same size) is equivalent by elementary methods to the version with one set:

Here's one trick that will work if you need A',B' to be different: if E(A,B) is N^3/K say then by pigeonholing there is a set B', subset of some translate of B, of size at least N/K (and replacing B by a translate if necessary) you can deduce that 1_A*1_A is at least N/2K pointwise on B'. Now Cauchy-Schwarz implies E(A,B') is at least N^3/4K^2, and apply the version of BSG that Yael has formalised to find some B'' inside B' with small doubling. But by averaging some translate of B'' has intersection at least N/K^c with A, let this be A''. Now we have sets A'' in A and B'' in B (or some translates of them) such that |A''+B''| \leq |B''+B''| and done.

Alternatively the proof that Yael has formalised adapts very easily to the case of two sets anyway, so probably easier to just copy and paste that proof and change some sets to be different.

[Yaël Dillies]

Is the two sets version strictly more general?

[Thomas Bloom]

Yaël Dillies said:

Is the two sets version strictly more general?

In a qualitative sense yes, but it's quantitatively a little different, if you care about the exponents.

[Yaël Dillies]

Okay, I see, the proof in LeanAPAP already gives the stronger result so I might as well adapt it

[Daniel Weber]

Thanks! By the way, was Ruzsa calculus formalized in Lean? I saw PFR has entropic Rusza calculus, I guess the set version can be derieved from it?

[Yaël Dillies]

Yes, we have Ruzsa calculus in mathlib already, see file#Combinatorics/Additive/PluenneckeRuzsa

[Daniel Weber]

Ok, thanks!

[Mario Carneiro]

@Yaël Dillies said:

(btw it would be nice if LeanAPAP#BSG could be linkified)

[Daniel Weber]

Yaël Dillies said:

Okay, I see, the proof in LeanAPAP already gives the stronger result so I might as well adapt it

Sorry to bother you, but are you planning on doing this soon or should I do it?

[Daniel Weber]

@Yaël Dillies ?

[Yaël Dillies]

Sorry, have had no time to fix it! Feel free to open a PR if you know how to

[Daniel Weber]

Ok. Would you mind sending a reference to the proof you formalized?

[Yaël Dillies]

Here it is: SimpleBSG.pdf

[Daniel Weber]

Thanks! I might be missing something, but from the proof we have that $A'$ is a subset of a translate of $B$, so it should be possible to just translate it back to get our $B'$, right? I'll try formalizing this

[Yaël Dillies]

Yes, that's basically what Tom said above

[Daniel Weber]

Yaël Dillies said:

Sorry, have had no time to fix it! Feel free to open a PR if you know how to

:+1: I opened https://github.com/YaelDillies/LeanAPAP/pull/6