OAI/Combinatorics/SharpRamsey/Learning/TestLearningIncidence.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SharpLogRamsey.ProjectiveDuality.dual_variance_le line 20
2. lemma OAI.SharpLogRamsey.RegularPencils.square_tail_card line 42
3. theorem OAI.SharpLogRamsey.RegularPencils.pencil_weight_tail line 61
4. theorem OAI.SharpLogRamsey.RegularPencils.pencil_family_tail line 89
5. def OAI.SharpLogRamsey.PencilContrast.degree line 119
6. lemma OAI.SharpLogRamsey.PencilContrast.sum_degree line 122
7. theorem OAI.SharpLogRamsey.PencilContrast.support_large_degree line 126
8. theorem OAI.SharpLogRamsey.PencilContrast.ambient_small_degree line 157