OAI/Geometry/ProjectionBodies/Model.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PettyProjection.Space line 11

   Also declared: ComparatorChallenges/PettyProjectionVolume.lean:11 (same declaration text).

2. def OAI.PettyProjection.IsConvexBody line 13

   Also declared: ComparatorChallenges/PettyProjectionVolume.lean:13 (same declaration text).

3. def OAI.PettyProjection.unitBall line 16

   Also declared: ComparatorChallenges/PettyProjectionVolume.lean:16 (same declaration text).

4. def OAI.PettyProjection.kappa line 18

   Also declared: ComparatorChallenges/PettyProjectionVolume.lean:18 (same declaration text).

5. def OAI.PettyProjection.perpendicular line 20

   Also declared: ComparatorChallenges/PettyProjectionVolume.lean:20 (same declaration text).

6. def OAI.PettyProjection.shadowVolume line 24

   Source documentation

   Volume in the induced Euclidean structure on the orthogonal hyperplane.

   Also declared: ComparatorChallenges/PettyProjectionVolume.lean:24 (same declaration text).

   def shadowVolume {n : ℕ} (K : Set (Space n)) (u : Space n) : ℝ :=
   …

   Mentions: OAI.PettyProjection.Space

7. def OAI.PettyProjection.projectionBody line 30

   Source documentation

   The body with support function equal to the volumes of orthogonal shadows, expressed as its defining intersection of supporting half-spaces.

   Also declared: ComparatorChallenges/PettyProjectionVolume.lean:30 (same declaration text).

   def projectionBody {n : ℕ} (K : Set (Space n)) : Set (Space n) :=
   …

   Mentions: OAI.PettyProjection.Space

8. def OAI.PettyProjection.projectionRatio line 33

   Also declared: ComparatorChallenges/PettyProjectionVolume.lean:33 (same declaration text).

9. def OAI.PettyProjection.pettyConstant line 36

   Also declared: ComparatorChallenges/PettyProjectionVolume.lean:36 (same declaration text).

10. def OAI.PettyProjection.IsEllipsoid line 39

    Also declared: ComparatorChallenges/PettyProjectionVolume.lean:39 (same declaration text).

11. def OAI.PettyProjection.MainClaim line 43