OAI/Combinatorics/MatchingEntropy/Model.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.MatchingEntropyBounds.LooplessGraph line 14

   Also declared: ComparatorChallenges/MatchingEntropyBounds.lean:14 (same declaration text), ComparatorChallenges/TriangleFace.lean:14 (same declaration text).

2. def OAI.MatchingEntropyBounds.LooplessGraph.Incident line 24

   Also declared: ComparatorChallenges/MatchingEntropyBounds.lean:24 (same declaration text), ComparatorChallenges/TriangleFace.lean:24 (same declaration text).

3. instance OAI.MatchingEntropyBounds.LooplessGraph.incidentDecidable line 27

   Also declared: ComparatorChallenges/MatchingEntropyBounds.lean:27 (same declaration text), ComparatorChallenges/TriangleFace.lean:27 (same declaration text).

4. def OAI.MatchingEntropyBounds.LooplessGraph.IsPerfectMatching line 30

   Also declared: ComparatorChallenges/MatchingEntropyBounds.lean:30 (same declaration text), ComparatorChallenges/TriangleFace.lean:30 (same declaration text).

5. abbrev OAI.MatchingEntropyBounds.LooplessGraph.Matching line 33

   Also declared: ComparatorChallenges/MatchingEntropyBounds.lean:33 (same declaration text), ComparatorChallenges/TriangleFace.lean:33 (same declaration text).

6. instance OAI.MatchingEntropyBounds.LooplessGraph.matchingFintype line 35

   Also declared: ComparatorChallenges/MatchingEntropyBounds.lean:35 (same declaration text), ComparatorChallenges/TriangleFace.lean:35 (same declaration text).

7. def OAI.MatchingEntropyBounds.LooplessGraph.indicator line 38

   Also declared: ComparatorChallenges/MatchingEntropyBounds.lean:38 (same declaration text), ComparatorChallenges/TriangleFace.lean:38 (same declaration text).

8. def OAI.MatchingEntropyBounds.LooplessGraph.polytope line 41

   Also declared: ComparatorChallenges/MatchingEntropyBounds.lean:41 (same declaration text), ComparatorChallenges/TriangleFace.lean:41 (same declaration text).

9. def OAI.MatchingEntropyBounds.LooplessGraph.mean line 44

   Also declared: ComparatorChallenges/MatchingEntropyBounds.lean:44 (same declaration text).

10. def OAI.MatchingEntropyBounds.probabilitySimplex line 49

    Also declared: ComparatorChallenges/MatchingEntropyBounds.lean:49 (same declaration text).

11. def OAI.MatchingEntropyBounds.LooplessGraph.feasibleLaws line 54

    Distinct definitions of this name: ComparatorChallenges/MatchingEntropyBounds.lean:52 (different declaration text). Qualify references as OAI.MatchingEntropyBounds.LooplessGraph.feasibleLaws@path.

12. def OAI.MatchingEntropyBounds.entropy line 59

    Also declared: ComparatorChallenges/MatchingEntropyBounds.lean:55 (same declaration text).

13. def OAI.MatchingEntropyBounds.maxMatchingEntropy line 62

    Also declared: ComparatorChallenges/MatchingEntropyBounds.lean:58 (same declaration text).

14. def OAI.MatchingEntropyBounds.Refined.complementEntropy line 67

    Also declared: ComparatorChallenges/MatchingEntropyBounds.lean:63 (same declaration text).