## 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

### 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 the 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.