OAI/Combinatorics/RamseyFive/Geometry/ProjectiveExpectedLevelLoss.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SharpRamseyFive.ProjectiveIncidence.projective_expected_level_loss line 15
2. lemma OAI.SharpRamseyFive.ProjectiveIncidence.Q_le_power line 64
3. lemma OAI.SharpRamseyFive.ProjectiveIncidence.point_entropy_cap line 72
4. lemma OAI.SharpRamseyFive.ProjectiveIncidence.dual_entropy_cap line 83
5. theorem OAI.SharpRamseyFive.ProjectiveIncidence.projective_level_entropy line 94
6. theorem OAI.SharpRamseyFive.ProjectiveIncidence.endpoint_supports line 104