OAI/Combinatorics/RamseyFive/Geometry/HighPairVariance.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpRamseyFive.ProjectiveIncidence.relationMass_good_incident line 16
2. theorem OAI.SharpRamseyFive.ProjectiveIncidence.high_pair_incident_lower line 37
3. abbrev OAI.SharpRamseyFive.HighSamples.SampleFlag line 94
4. def OAI.SharpRamseyFive.HighSamples.growSpan line 96
5. lemma OAI.SharpRamseyFive.HighSamples.le_growSpan line 101
6. lemma OAI.SharpRamseyFive.HighSamples.hit_le_growSpan line 105
7. lemma OAI.SharpRamseyFive.HighSamples.rank_growSpan_mono line 113
8. lemma OAI.SharpRamseyFive.HighSamples.growSpan_eq_of_rank_le line 118
9. lemma OAI.SharpRamseyFive.HighSamples.small_subspace_card line 125
10. def OAI.SharpRamseyFive.HighSamples.newHits line 140
11. lemma OAI.SharpRamseyFive.HighSamples.first_incident_mass line 145
12. lemma OAI.SharpRamseyFive.HighSamples.second_subspace_mass line 156
13. theorem OAI.SharpRamseyFive.HighSamples.newHits_mass line 175