OAI/Geometry/ProjectionVolume/SimplexProjection.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Paper092.projection_eq_iff_parallel line 18
  2. theorem OAI.Paper092.mem_projection_iff_line_meets line 32
  3. theorem OAI.Paper092.exists_step_to_boundary line 48
  4. def OAI.Paper092.simplexCoordinates line 72
  5. def OAI.Paper092.simplexVelocity line 76
  6. theorem OAI.Paper092.simplexCoordinates_nonneg_iff line 80
  7. theorem OAI.Paper092.simplexCoordinates_add_smul line 91
  8. theorem OAI.Paper092.simplexVelocity_neg_exists line 102
  9. theorem OAI.Paper092.exists_simplex_front_point line 115
  10. theorem OAI.Paper092.projection_injective_on_simplex_front line 126
  11. theorem OAI.Paper092.mem_standardSimplex_iff_coordinates line 148
  12. theorem OAI.Paper092.mem_simplex_projection_iff line 152
  13. def OAI.Paper092.simplexFacet line 160
  14. theorem OAI.Paper092.simplex_projection_eq_front_cover line 163
  15. theorem OAI.Paper092.front_facets_projection_inter_eq line 179
  16. def OAI.Paper092.simplexCoordinateAffine line 195
  17. theorem OAI.Paper092.simplexCoordinateAffine_apply line 200
  18. def OAI.Paper092.simplexVertex line 204
  19. theorem OAI.Paper092.simplexCoordinates_vertex line 208
  20. theorem OAI.Paper092.facet_seam_projection_invariant line 212
  21. theorem OAI.Paper092.projected_facet_seam_null line 227
  22. theorem OAI.Paper092.projected_front_facets_aedisjoint line 261
  23. theorem OAI.Paper092.simplexFacet_isCompact line 277
  24. theorem OAI.Paper092.projected_simplexFacet_isCompact line 287
  25. theorem OAI.Paper092.projectionVolume_simplex_eq_front_sum line 291
  26. theorem OAI.Paper092.brightness_simplex_eq_front_sum line 308