OAI/Analysis/SegmentLenses/Gates.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Exterior gates and disjoint cone regions

  1. theorem OAI.SegmentLenses.exists_gate_below line 24
  2. theorem OAI.SegmentLenses.gate_below_unique line 42
  3. abbrev OAI.SegmentLenses.ExteriorVertex line 49
  4. def OAI.SegmentLenses.exteriorGate line 52
  5. theorem OAI.SegmentLenses.exteriorGate_le line 55
  6. def OAI.SegmentLenses.exteriorPartition line 58
  7. theorem OAI.SegmentLenses.exteriorGate_eq_iff line 67
  8. def OAI.SegmentLenses.exteriorEmbedding line 75
  9. theorem OAI.SegmentLenses.exteriorEmbedding_range line 79
  10. theorem OAI.SegmentLenses.exterior_testTail line 85
  11. theorem OAI.SegmentLenses.exterior_primalTail line 101
  12. theorem OAI.SegmentLenses.primalTail_exterior line 110
  13. def OAI.SegmentLenses.exteriorDual line 115
  14. theorem OAI.SegmentLenses.norm_exteriorDual line 120