# Lean Bourgain

The purpose of this repository is to formalize the Bourgain extractor [Bou05], and as a part of that Szemeredi-Trotter in finite fields ([BKT04]), in Lean 4.

## The source

Most definitions, theorems and proofs in this project have been taken from [Dvi12].

Additionally, some proofs were taken from the course “Selected Topics in Pseudorandomess” in Ben-Gurion University of the Negev, which exposed me to this subject and this formalization was a project for, and the proofs about the generalized XOR lemma were taken from [Rao07].

I remember seeing the proof used for showing every source is a convex combination of flat sources, by repeatedly taking a flat source of the highest K values with the maximum possibile coefficient, in some paper, but I couldn’t locate it. If anyone is aware where this proof appeared, please inform me.

## The result

The final result of this project is bourgain_extractor_final, which states that for any prime \(p\), not equal to 2, and any positive integer \(m\), the function \(f(x, y) = (xy + x^2 y^2 \bmod p) \bmod{m}\) is a two source extractor, with \(k = (1/2 - 1/35686629198734977) \log(p),\) and \(\varepsilon = C p^{-1/2283944268719038528} \sqrt{m} (3 \ln(p) + 3) + \frac{m}{2p},\) where \(C = \left( 16 \left(\sqrt{2\left((4\sqrt{16(2^{49}+2) + 5} + 92)^{1/4} + \frac{\sqrt2}4\right)} + 1\right) + 1\right)^{1/64} \approx 1.09 .\) It can be noted that these values are quite worse than what appears in the literature, which I believe is mostly due to not attempting to optimize them at all.

## Acknowledgements

I’d like to thank Dean Doron for introducting me to this interesting subject, pointing me to the relevant papers, and helping with anything I had trouble understanding in them.

I’d like to thank the Lean community for helping me with any problems I had with Lean.

Finally, I’d like to thank Yaël Dillies for LeanAPAP, whose results on discrete analysis had been extremely helpful.

## Infrastructure

The infrastructure for this webpage was mostly taken from LeanAPAP and PFR.

## Sources

[Bou05]: Bourgain, J. (2005). MORE ON THE SUM-PRODUCT PHENOMENON IN PRIME FIELDS AND ITS APPLICATIONS. International Journal of Number Theory, 01, 1-32.

[BKT04]: Bourgain, J., Katz, N.H., & Tao, T. (2004). A sum-product estimate in finite fields, and applications. Geometric & Functional Analysis GAFA, 14, 27-57.

[Dvi12]: Dvir, Z. (2012). Incidence Theorems and Their Applications. Found. Trends Theor. Comput. Sci., 6, 257-393.

[Rao07]: Rao, A. (2007). An Exposition of Bourgain’s 2-Source Extractor. Electron. Colloquium Comput. Complex., TR07.