OAI/Geometry/PolarProducts/Model.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SymmetricPolar.Position line 11

   Also declared: ComparatorChallenges/SymmetricPolar.lean:10 (same declaration text).

2. abbrev OAI.SymmetricPolar.Phase line 12

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

3. def OAI.SymmetricPolar.IsSymmetricConvexBody line 14

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

4. def OAI.SymmetricPolar.polar line 18

   Also declared: ComparatorChallenges/SymmetricPolar.lean:17 (same declaration text).

5. def OAI.SymmetricPolar.polarProduct line 21

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

6. def OAI.SymmetricPolar.capacityBall line 24

   Also declared: ComparatorChallenges/SymmetricPolar.lean:23 (same declaration text).

7. def OAI.SymmetricPolar.omega0 line 27

   Also declared: ComparatorChallenges/SymmetricPolar.lean:26 (same declaration text).

8. def OAI.SymmetricPolar.HasSymplecticEmbedding line 30

   Also declared: ComparatorChallenges/SymmetricPolar.lean:29 (same declaration text).

9. def OAI.SymmetricPolar.gromovWidth line 38

   Also declared: ComparatorChallenges/SymmetricPolar.lean:37 (same declaration text).