OAI/Analysis/Cotype/Model.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Cotype.Cube line 10

   Also declared: ComparatorChallenges/Cotype.lean:12 (same declaration text).

2. def OAI.Cotype.sign line 12

   Also declared: ComparatorChallenges/Cotype.lean:14 (same declaration text).

3. def OAI.Cotype.average line 14

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

4. def OAI.Cotype.cubeL2 line 19

   Also declared: ComparatorChallenges/Cotype.lean:21 (same declaration text).

5. def OAI.Cotype.rademacherSum line 22

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

6. def OAI.Cotype.moment line 25

   Also declared: ComparatorChallenges/Cotype.lean:27 (same declaration text).

7. def OAI.Cotype.radProjection line 28

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

8. def OAI.Cotype.KConvex line 31

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

9. def OAI.Cotype.HasCotype line 34

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

10. def OAI.Cotype.FiniteCotype line 38

    Also declared: ComparatorChallenges/Cotype.lean:40 (same declaration text).

11. def OAI.Cotype.ApproximationProperty line 40

    Also declared: ComparatorChallenges/Cotype.lean:42 (same declaration text).

12. def OAI.Cotype.MainTarget line 45

    Distinct definitions of this name: ComparatorChallenges/Cotype.lean:47 (same statement text; different proof or body). Qualify references as OAI.Cotype.MainTarget@path.