OAI/Probability/LatticeSurface/Coercivity/SparseModel.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SparseBlocks.Adj line 167
  2. def OAI.SparseBlocks.latticeDist line 172
  3. def OAI.SparseBlocks.height line 176
  4. def OAI.SparseBlocks.body line 179
  5. def OAI.SparseBlocks.block line 182
  6. def OAI.SparseBlocks.enlarged line 186
  7. def OAI.SparseBlocks.face line 190
  8. def OAI.SparseBlocks.neighbor line 195
  9. def OAI.SparseBlocks.bad line 200
  10. def OAI.SparseBlocks.thickBad line 208
  11. lemma OAI.SparseBlocks.adj_symm line 218
  12. lemma OAI.SparseBlocks.adj_ne line 221
  13. def OAI.SparseBlocks.finiteGraph line 224
  14. def OAI.SparseBlocks.fixed line 227
  15. def OAI.SparseBlocks.indexEquiv line 229
  16. def OAI.SparseBlocks.coordinates line 235
  17. lemma OAI.SparseBlocks.preserving_coordinates line 239
  18. lemma OAI.SparseBlocks.coordinates_height line 243
  19. lemma OAI.SparseBlocks.body_coordinates line 255
  20. lemma OAI.SparseBlocks.continuous_height line 273
  21. lemma OAI.SparseBlocks.closed_body line 280
  22. lemma OAI.SparseBlocks.volume_body_coordinates line 285