OAI/Probability/LatticeSurface/Geometry/EdgeCoordinates.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EdgeCoordinates.shear line 13
  2. lemma OAI.EdgeCoordinates.shear_zero line 39
  3. lemma OAI.EdgeCoordinates.shear_succ line 42
  4. lemma OAI.EdgeCoordinates.shear_symm_zero line 45
  5. lemma OAI.EdgeCoordinates.shear_symm_succ line 48
  6. lemma OAI.EdgeCoordinates.shear_measurePreserving line 51
  7. lemma OAI.EdgeCoordinates.norm_shear_le line 71
  8. lemma OAI.EdgeCoordinates.norm_shear_symm_le line 86
  9. def OAI.EdgeCoordinates.signedShear line 102
  10. lemma OAI.EdgeCoordinates.signedShear_measurePreserving line 106
  11. lemma OAI.EdgeCoordinates.norm_signedShear_le line 114
  12. lemma OAI.EdgeCoordinates.norm_signedShear_symm_le line 118
  13. lemma OAI.EdgeCoordinates.exists_indexEquiv line 128
  14. def OAI.EdgeCoordinates.reindex line 136
  15. lemma OAI.EdgeCoordinates.reindex_apply line 139
  16. lemma OAI.EdgeCoordinates.norm_reindex line 142
  17. lemma OAI.EdgeCoordinates.norm_reindex_symm line 152
  18. lemma OAI.EdgeCoordinates.reindex_measurePreserving line 156
  19. def OAI.EdgeCoordinates.edgeMap line 160
  20. lemma OAI.EdgeCoordinates.edgeMap_measurePreserving line 164
  21. lemma OAI.EdgeCoordinates.norm_edgeMap_symm_le line 169
  22. lemma OAI.EdgeCoordinates.edgeMap_zero line 179
  23. lemma OAI.EdgeCoordinates.exists_edge_coordinates line 185