OAI/Probability/LatticeSurface/Geometry/TriangularGeometry.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TriangularLipschitz.latticeDist line 14
  2. def OAI.TriangularLipschitz.box line 18
  3. def OAI.TriangularLipschitz.interior line 21
  4. abbrev OAI.TriangularLipschitz.Filling line 24
  5. def OAI.TriangularLipschitz.filledHeight line 26
  6. def OAI.TriangularLipschitz.fillingPolytope line 30
  7. def OAI.TriangularLipschitz.fillingVolume line 34
  8. def OAI.TriangularLipschitz.logFillingVolume line 37
  9. def OAI.TriangularLipschitz.positiveLogVolume line 41
  10. def OAI.TriangularLipschitz.faceCenter line 44
  11. def OAI.TriangularLipschitz.compressedNeighbor line 51
  12. def OAI.TriangularLipschitz.ConvexGood line 58
  13. lemma OAI.TriangularLipschitz.adj_symm line 64
  14. lemma OAI.TriangularLipschitz.adj_ne line 69
  15. def OAI.TriangularLipschitz.latticeGraph line 76
  16. abbrev OAI.TriangularLipschitz.BoxVertex line 81
  17. def OAI.TriangularLipschitz.boxGraph line 83
  18. lemma OAI.TriangularLipschitz.boxGraph_adj line 85
  19. lemma OAI.TriangularLipschitz.mem_box line 88
  20. instance OAI.TriangularLipschitz.box_nonempty line 92
  21. def OAI.TriangularLipschitz.intDist line 95
  22. lemma OAI.TriangularLipschitz.intDist_nonneg line 98
  23. lemma OAI.TriangularLipschitz.intDist_eq_zero_iff line 101
  24. lemma OAI.TriangularLipschitz.intDist_cast line 106
  25. lemma OAI.TriangularLipschitz.geodesic_step line 109
  26. lemma OAI.TriangularLipschitz.box_geodesic line 153
  27. lemma OAI.TriangularLipschitz.box_connected line 185
  28. lemma OAI.TriangularLipschitz.latticeDist_triangle line 191
  29. lemma OAI.TriangularLipschitz.intDist_adj line 209
  30. lemma OAI.TriangularLipschitz.latticeDist_adj line 215
  31. lemma OAI.TriangularLipschitz.latticeDist_walk_le line 219
  32. lemma OAI.TriangularLipschitz.box_dist line 230
  33. lemma OAI.TriangularLipschitz.scaled_edge_bound_walk line 242
  34. lemma OAI.TriangularLipschitz.near_global_bound line 255