OAI/Analysis/MetricEntropy/Model.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MetricEntropyDuality.RealSpace line 17

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

2. def OAI.MetricEntropyDuality.pairing line 19

   Also declared: ComparatorChallenges/MetricEntropyDuality.lean:19 (same declaration text).

3. def OAI.MetricEntropyDuality.cube line 22

   Also declared: ComparatorChallenges/MetricEntropyDuality.lean:22 (same declaration text).

4. def OAI.MetricEntropyDuality.polar line 25

   Also declared: ComparatorChallenges/MetricEntropyDuality.lean:25 (same declaration text).

5. def OAI.MetricEntropyDuality.Covers line 28

   Also declared: ComparatorChallenges/MetricEntropyDuality.lean:28 (same declaration text).

6. def OAI.MetricEntropyDuality.Coverable line 32

   Also declared: ComparatorChallenges/MetricEntropyDuality.lean:32 (same declaration text).

7. def OAI.MetricEntropyDuality.coveringNumber line 35

   Also declared: ComparatorChallenges/MetricEntropyDuality.lean:35 (same declaration text).

8. structure OAI.MetricEntropyDuality.IsSymmetricConvexBody line 38

   Also declared: ComparatorChallenges/MetricEntropyDuality.lean:38 (same declaration text).