OAI/Geometry/ProjectionVolume/BallBrightness.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Paper092.euclideanUnitBallVolume line 12
2. theorem OAI.Paper092.projection_image_closedBall line 15
3. theorem OAI.Paper092.projectionVolume_closedBall_real line 28
4. theorem OAI.Paper092.brightness_closedBall line 50
5. theorem OAI.Paper092.brightness_le_ball_bound line 59
6. theorem OAI.Paper092.ball_subset_projectionBody line 65
7. theorem OAI.Paper092.projectionBody_subset_ball line 77