OAI/Probability/LatticeSurface/Coercivity/HoleSize.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SparseHoles.natAbs_sub_triangle line 20
  2. lemma OAI.SparseHoles.star_walk_bounds line 24
  3. lemma OAI.SparseHoles.cluster_pair_bounds line 36
  4. def OAI.SparseHoles.offsetBox line 54
  5. lemma OAI.SparseHoles.natAbs_sub_le_iff line 57
  6. lemma OAI.SparseHoles.mem_offsetBox line 62
  7. lemma OAI.SparseHoles.offsetBox_card line 67
  8. lemma OAI.SparseHoles.filled_in_cluster_ball line 74
  9. def OAI.SparseHoles.diameter line 81
  10. lemma OAI.SparseHoles.le_diameter line 84
  11. lemma OAI.SparseHoles.diameter_le line 93
  12. lemma OAI.SparseHoles.card_le_diameter_sq line 102
  13. lemma OAI.SparseHoles.filled_diameter_le line 111
  14. def OAI.SparseHoles.incidentClosed line 128
  15. lemma OAI.SparseHoles.incident_filled_location line 130