OAI/Analysis/SegmentLenses/Embeddings.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Segment embeddings and convex tree regions

  1. structure OAI.SegmentLenses.SegmentEmbedding line 24
  2. def OAI.SegmentLenses.SegmentEmbedding.testMap line 34
  3. theorem OAI.SegmentLenses.SegmentEmbedding.testMap_apply line 44
  4. theorem OAI.SegmentLenses.SegmentEmbedding.testMap_sum line 50
  5. theorem OAI.SegmentLenses.SegmentEmbedding.norm_testMap line 59
  6. def OAI.SegmentLenses.SegmentEmbedding.testIsometry line 106
  7. def OAI.SegmentLenses.convexSegmentEmbedding line 121
  8. def OAI.SegmentLenses.Region.Vertex line 178
  9. instance OAI.SegmentLenses.Region.(instance at line 181) line 181
  10. instance OAI.SegmentLenses.Region.(instance at line 182) line 182
  11. instance OAI.SegmentLenses.Region.(instance at line 185) line 185
  12. instance OAI.SegmentLenses.Region.(instance at line 192) line 192
  13. instance OAI.SegmentLenses.Region.(instance at line 195) line 195
  14. instance OAI.SegmentLenses.Region.(instance at line 203) line 203
  15. instance OAI.SegmentLenses.Region.(instance at line 213) line 213
  16. def OAI.SegmentLenses.Region.inclusion line 215
  17. theorem OAI.SegmentLenses.Region.range_inclusion line 220
  18. def OAI.SegmentLenses.Region.embedding line 227
  19. def OAI.SegmentLenses.SegmentEmbedding.primalMap line 239
  20. theorem OAI.SegmentLenses.SegmentEmbedding.primalMap_test line 243
  21. theorem OAI.SegmentLenses.SegmentEmbedding.norm_primalMap line 248
  22. def OAI.SegmentLenses.SegmentEmbedding.primalIsometry line 255
  23. theorem OAI.SegmentLenses.SegmentEmbedding.primalMap_unitVector line 258