OAI/Combinatorics/SharpRamsey/Geometry/ProjectionCenterTools.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLogRamsey.Projection.cut line 13
2. lemma OAI.SharpLogRamsey.Projection.cut_card_sum line 20
3. lemma OAI.SharpLogRamsey.Projection.surviving_incidence_sum line 35
4. lemma OAI.SharpLogRamsey.Projection.cut_variance line 55
5. lemma OAI.SharpLogRamsey.FiniteAveraging.exists_small line 84
6. lemma OAI.SharpLogRamsey.FiniteAveraging.exists_five line 92
7. theorem OAI.SharpLogRamsey.Projection.exists_center line 117