OAI/Probability/LatticeSurface/Coercivity/HoleLocal.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SparseHoles.activeHoles line 23
  2. def OAI.SparseHoles.localEdges line 27
  3. lemma OAI.SparseHoles.HoleFamily.mono line 33
  4. lemma OAI.SparseHoles.active_subset line 41
  5. lemma OAI.SparseHoles.active_mem line 44
  6. lemma OAI.SparseHoles.active_fill line 49
  7. lemma OAI.SparseHoles.active_edgeAbs line 60
  8. lemma OAI.SparseHoles.weights_mono line 68
  9. lemma OAI.SparseHoles.local_edges_good line 79
  10. lemma OAI.SparseHoles.local_energy_bound line 91
  11. lemma OAI.SparseHoles.rim_in_buffer line 114
  12. lemma OAI.SparseHoles.local_edges_buffer line 136
  13. lemma OAI.SparseHoles.local_hole_energy line 161