OAI/Geometry/ProjectionVolume/AffineBrightness.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Paper092.normalFrameVector line 19
  2. theorem OAI.Paper092.normalFrameVector_orthonormal line 25
  3. def OAI.Paper092.normalFrame line 42
  4. theorem OAI.Paper092.normalFrame_inl line 55
  5. theorem OAI.Paper092.normalFrame_inr line 61
  6. def OAI.Paper092.projectionTransport line 67
  7. theorem OAI.Paper092.projectionTransport_matrix line 72
  8. theorem OAI.Paper092.projectionTransport_normDet line 108
  9. theorem OAI.Paper092.projectionTransport_project line 133
  10. theorem OAI.Paper092.projection_image_linearEquiv line 153
  11. theorem OAI.Paper092.projectionVolume_linearEquiv_image line 160
  12. theorem OAI.Paper092.brightness_linearEquiv_image line 176