OAI/Probability/LatticeSurface/Coercivity/HoleTail.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SparseHoles.badGraph line 28
2. def OAI.SparseHoles.holes line 33
3. lemma OAI.SparseHoles.star_offset line 44
4. lemma OAI.SparseHoles.finite_star_degree line 54
5. lemma OAI.SparseHoles.cluster_component_bound line 66
6. lemma OAI.SparseHoles.large_diameter_witness line 79
7. lemma OAI.SparseHoles.ambient_component_tail line 122
8. lemma OAI.SparseHoles.quadratic_le_geometric line 150
9. lemma OAI.SparseHoles.roots_card line 160
10. lemma OAI.SparseHoles.hole_diameter_tail line 173