OAI/Geometry/ProjectionVolume/Brightness.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Paper092.normalHyperplane_smul line 10
  2. theorem OAI.Paper092.projectionVolume_smul line 15
  3. theorem OAI.Paper092.brightness_smul line 20
  4. theorem OAI.Paper092.brightness_neg line 27
  5. theorem OAI.Paper092.brightness_nonneg line 31
  6. theorem OAI.Paper092.zero_mem_projectionBody line 34
  7. theorem OAI.Paper092.neg_mem_projectionBody_iff line 39
  8. theorem OAI.Paper092.projectionBody_neg_eq line 47
  9. theorem OAI.Paper092.projectionVolume_lt_top line 52
  10. theorem OAI.Paper092.projectionVolume_mono line 56
  11. theorem OAI.Paper092.brightness_mono line 60
  12. theorem OAI.Paper092.projectionBody_mono line 66
  13. theorem OAI.Paper092.projectionBody_isClosed line 70
  14. theorem OAI.Paper092.projectionBody_convex line 75
  15. theorem OAI.Paper092.projectionBody_norm_le line 80
  16. theorem OAI.Paper092.projectionBody_isCompact line 97
  17. theorem OAI.Paper092.projectionVolume_body_smul line 103
  18. theorem OAI.Paper092.brightness_body_smul line 110
  19. theorem OAI.Paper092.projectionBody_body_smul line 118