OAI/Probability/LatticeSurface/Coercivity/HoleExtension.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SparseHoles.representative line 22
  2. def OAI.SparseHoles.fillSite line 27
  3. def OAI.SparseHoles.extension line 31
  4. structure OAI.SparseHoles.HoleFamily line 34
  5. def OAI.SparseHoles.siteDiameter line 42
  6. def OAI.SparseHoles.edgeDiameter line 46
  7. def OAI.SparseHoles.goodSite line 49
  8. def OAI.SparseHoles.goodEdge line 51
  9. def OAI.SparseHoles.holeCost line 54
  10. def OAI.SparseHoles.holeWeights line 57
  11. lemma OAI.SparseHoles.representative_mem line 61
  12. lemma OAI.SparseHoles.fillSite_good line 73
  13. lemma OAI.SparseHoles.fillSite_hole line 79
  14. lemma OAI.SparseHoles.outer_hole_family line 90
  15. lemma OAI.SparseHoles.neighbor_of_hole_good line 104
  16. lemma OAI.SparseHoles.incident_outside_rim line 112
  17. lemma OAI.SparseHoles.crossing_power line 116
  18. lemma OAI.SparseHoles.same_hole_edge line 129
  19. lemma OAI.SparseHoles.rim_edge_good line 134
  20. lemma OAI.SparseHoles.diameter_le_site line 141
  21. lemma OAI.SparseHoles.rim_diameter_le_edge line 147
  22. lemma OAI.SparseHoles.rim_overlap line 157
  23. lemma OAI.SparseHoles.holeCost_nonneg line 182
  24. lemma OAI.SparseHoles.holeCost_bound line 186
  25. lemma OAI.SparseHoles.weights_bound line 210
  26. lemma OAI.SparseHoles.power_hole_edge_bound line 239
  27. lemma OAI.SparseHoles.edge_power_bound line 264
  28. lemma OAI.SparseHoles.sum_incident_bound line 293
  29. lemma OAI.SparseHoles.extension_sum_bound line 303
  30. lemma OAI.SparseHoles.weighted_sum_identity line 327
  31. theorem OAI.SparseHoles.hole_extension_energy line 351