Discussion about the Bourgain Extractor

Stream: general

[Yaël Dillies]

Discussion thread for https://leanprover.zulipchat.com/#narrow/stream/113486-announce/topic/The.20Bourgain.20Extractor

[Yaël Dillies]

Congrats, @Daniel Weber! What's your plan for integration in mathlib? I see that quite a lot of definitions could be upstreamed to LeanAPAP at least

[Daniel Weber]

Yaël Dillies said:

Congrats, Daniel Weber! What's your plan for integration in mathlib? I see that quite a lot of definitions could be upstreamed to LeanAPAP at least

Thanks! I'm not quite sure yet, as there's a lot I want to clean up, but:

• Most of Pseudorandom.Additive.Main could probably go fairly directly to Mathlib, and maybe some of the other additive combinatorics stuff.
• Pseudorandom.Util can go to an appropriate places in Mathlib, after making it a bit more general.
• Pseudorandom.LpLemmas can go to LeanAPAP and eventually to Mathlib.
• Is transfer (for $f: A \to B$ and $g: A \to C$ we look at $h:B \to C$ defined by $h(x) = \sum_{f(y) = x} g(y)$) defined somewhere in Mathlib that I missed? If not it can be moved there.
• Regarding Szemeredi-Trotter in prime fields I'm not quite sure yet, but maybe it could eventually be moved to Mathlib.
• The rest of the results depend on FinPMF, and I saw the discussion in https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Should.20there.20be.20a.20ProbabilitySpace.20class.3F about how discrete probability should be handled in Mathlib—I think it should be resolved before any of those results could be incorporated.