OAI/Combinatorics/SharpRamsey/Learning/PreparedTypical.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpLogRamsey.PreparedTypical.outside_count line 13
2. lemma OAI.SharpLogRamsey.PreparedTypical.outside_scalar line 34
3. lemma OAI.SharpLogRamsey.PreparedTypical.outside_square line 46
4. def OAI.SharpLogRamsey.PreparedTypical.mass line 60
5. lemma OAI.SharpLogRamsey.PreparedTypical.outside_mass_between line 65
6. theorem OAI.SharpLogRamsey.PreparedTypical.typical_point line 83
7. theorem OAI.SharpLogRamsey.PreparedTypical.typical_squares line 92