OAI/Analysis/SegmentLenses/EndpointBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Endpoint bounds, clipping, and gate coordinates

  1. theorem OAI.SegmentLenses.endpoint_laws_on_gates line 27
  2. def OAI.SegmentLenses.lawSupport line 125
  3. theorem OAI.SegmentLenses.subset_lawSupport line 128
  4. theorem OAI.SegmentLenses.bounded_multiplier line 139
  5. def OAI.SegmentLenses.FiniteLaw.equalPair line 156
  6. theorem OAI.SegmentLenses.FiniteLaw.equalPair_expect line 161
  7. theorem OAI.SegmentLenses.nonzero_midpoint_bound line 172
  8. theorem OAI.SegmentLenses.subtype_l2_bound line 223
  9. theorem OAI.SegmentLenses.endpoint_laws_global line 258
  10. theorem OAI.SegmentLenses.gate_coordinate_l2 line 303