OAI/Combinatorics/KMedianRecovery/Model.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.MetricKMedianRecovery.RationalMetricInput line 7

   Also declared: ComparatorChallenges/KMedianRecovery.lean:7 (same declaration text), ComparatorChallenges/KMedianRefinedRecovery.lean:7 (same declaration text).

2. def OAI.MetricKMedianRecovery.RationalMetricInput.size line 23

   Also declared: ComparatorChallenges/KMedianRecovery.lean:23 (same declaration text), ComparatorChallenges/KMedianRefinedRecovery.lean:23 (same declaration text).

3. def OAI.MetricKMedianRecovery.RationalMetricInput.Feasible line 25

   Also declared: ComparatorChallenges/KMedianRecovery.lean:25 (same declaration text), ComparatorChallenges/KMedianRefinedRecovery.lean:25 (same declaration text).

4. def OAI.MetricKMedianRecovery.RationalMetricInput.cost line 28

   Also declared: ComparatorChallenges/KMedianRecovery.lean:28 (same declaration text), ComparatorChallenges/KMedianRefinedRecovery.lean:28 (same declaration text).

5. def OAI.MetricKMedianRecovery.RationalMetricInput.comparisonSets line 31

   Also declared: ComparatorChallenges/KMedianRecovery.lean:31 (same declaration text).

6. lemma OAI.MetricKMedianRecovery.RationalMetricInput.comparisonSets_nonempty line 34

   Also declared: ComparatorChallenges/KMedianRecovery.lean:34 (same declaration text).

7. def OAI.MetricKMedianRecovery.RationalMetricInput.optimum line 41

   Also declared: ComparatorChallenges/KMedianRecovery.lean:41 (same declaration text).

8. def OAI.MetricKMedianRecovery.RationalMetricInput.natBits line 44

   Also declared: ComparatorChallenges/KMedianRecovery.lean:44 (same declaration text), ComparatorChallenges/KMedianRefinedRecovery.lean:31 (same declaration text).

9. def OAI.MetricKMedianRecovery.RationalMetricInput.rationalBits line 47

   Also declared: ComparatorChallenges/KMedianRecovery.lean:47 (same declaration text), ComparatorChallenges/KMedianRefinedRecovery.lean:34 (same declaration text).

10. def OAI.MetricKMedianRecovery.RationalMetricInput.bits line 50

    Also declared: ComparatorChallenges/KMedianRecovery.lean:50 (same declaration text), ComparatorChallenges/KMedianRefinedRecovery.lean:37 (same declaration text).

11. def OAI.MetricKMedianRecovery.RationalMetricInput.decodeOutput line 57

    Also declared: ComparatorChallenges/KMedianRecovery.lean:57 (same declaration text), ComparatorChallenges/KMedianRefinedRecovery.lean:44 (same declaration text).

12. def OAI.MetricKMedianRecovery.pairBits line 62

    Also declared: ComparatorChallenges/KMedianRecovery.lean:62 (same declaration text), ComparatorChallenges/KMedianRefinedRecovery.lean:49 (same declaration text).

13. structure OAI.MetricKMedianRecovery.BinaryRandomizedAlgorithm line 65

    Also declared: ComparatorChallenges/KMedianRecovery.lean:65 (same declaration text), ComparatorChallenges/KMedianRefinedRecovery.lean:52 (same declaration text).

14. def OAI.MetricKMedianRecovery.BinaryRandomizedAlgorithm.bitCount line 73

    Also declared: ComparatorChallenges/KMedianRecovery.lean:73 (same declaration text).

15. abbrev OAI.MetricKMedianRecovery.BinaryRandomizedAlgorithm.Seed line 76

    Also declared: ComparatorChallenges/KMedianRecovery.lean:76 (same declaration text).

16. def OAI.MetricKMedianRecovery.BinaryRandomizedAlgorithm.output line 79

    Also declared: ComparatorChallenges/KMedianRecovery.lean:79 (same declaration text).

17. def OAI.MetricKMedianRecovery.BinaryRandomizedAlgorithm.successProbability line 83

    Also declared: ComparatorChallenges/KMedianRecovery.lean:83 (same declaration text).

18. def OAI.MetricKMedianRecovery.BinaryRandomizedAlgorithm.expectedCost line 89

    Also declared: ComparatorChallenges/KMedianRecovery.lean:89 (same declaration text).

19. def OAI.MetricKMedianRecovery.globalApplicationClaim line 94

    Also declared: ComparatorChallenges/KMedianRecovery.lean:94 (same declaration text).