OAI/Geometry/ProjectionBodies/Main.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PettyProjection.petty_projection_volume line 11

   Source documentation

   The exact unrestricted inequality and its global equality characterization.

   Distinct definitions of this name: ComparatorChallenges/PettyProjectionVolume.lean:45 (same statement text; different proof or body). Qualify references as OAI.PettyProjection.petty_projection_volume@path.

   theorem petty_projection_volume (n : ℕ) (hn : 4 ≤ n)
       (K : Set (Space n)) (hK : IsConvexBody K) :
       pettyConstant n ≤ projectionRatio K ∧
         (projectionRatio K = pettyConstant n ↔ IsEllipsoid K) := by
   …

   Mentions: OAI.PettyProjection.Space, OAI.PettyProjection.IsConvexBody, OAI.PettyProjection.pettyConstant, OAI.PettyProjection.projectionRatio, OAI.PettyProjection.IsEllipsoid

2. theorem OAI.PettyProjection.mainClaim_proved line 18
3. theorem OAI.PettyProjection.MainClaim_proved line 20