OAI/Combinatorics/SharpRamsey/Spatial/SpatialCost.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpLogRamsey.SpatialPublic.spatial_cost line 13
2. lemma OAI.SharpLogRamsey.SpatialPublic.spatial_log_card line 33
3. lemma OAI.SharpLogRamsey.SpatialPublic.eventually_header_budget line 54
4. lemma OAI.SharpLogRamsey.SpatialPublic.header_log_bound line 70
5. lemma OAI.SharpLogRamsey.SpatialPublic.heavy_header_cost line 111
6. lemma OAI.SharpLogRamsey.SpatialPublic.cover_log_bound line 136
7. lemma OAI.SharpLogRamsey.SpatialPublic.union_log_bound line 146