OAI/Geometry/ProjectionVolume/ProjectionJacobian.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Paper092.hyperplaneProjection line 19
2. lemma OAI.Paper092.normal_starProjection_unit line 23
3. lemma OAI.Paper092.det_one_sub_outer line 28
4. theorem OAI.Paper092.hyperplaneProjection_normDet line 33
5. theorem OAI.Paper092.volume_project_hyperplane line 72
6. theorem OAI.Paper092.projectionVolume_of_subset_affine_hyperplane line 105
7. theorem OAI.Paper092.brightness_of_subset_affine_hyperplane line 143