OAI/Combinatorics/KMedian/Hardness/Model.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.Complexity.FinitePolyTime line 9

   Source documentation

   Polynomial-time computation with every physical work alphabet finite.

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

   def FinitePolyTime {α β : Type} (ea : α → List Bool) (eb : β → List Bool)
       (f : α → β) : Prop :=
   …

2. abbrev OAI.MetricKMedian.Complexity.Word line 14

   Also declared: ComparatorChallenges/KMedianThreshold.lean:68 (same declaration text).

3. abbrev OAI.MetricKMedian.Complexity.Language line 15

   Also declared: ComparatorChallenges/KMedianThreshold.lean:69 (same declaration text).

4. def OAI.MetricKMedian.Complexity.encodeBit line 17

   Also declared: ComparatorChallenges/KMedianThreshold.lean:71 (same declaration text).

5. def OAI.MetricKMedian.Complexity.encodePair line 19

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

6. def OAI.MetricKMedian.Complexity.P line 22

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

7. def OAI.MetricKMedian.Complexity.NP line 25

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

8. def OAI.MetricKMedian.Complexity.PNeNP line 30

   Source documentation

   Separation of deterministic polynomial time from finite-verifier nondeterministic polynomial time.

   Also declared: ComparatorChallenges/KMedianThreshold.lean:84 (same declaration text).

   def PNeNP : Prop := P ≠ NP
   …

   Mentions: OAI.MetricKMedian.Complexity.P, OAI.MetricKMedian.Complexity.NP

9. def OAI.MetricKMedian.FactorCorrect line 34

   Source documentation

   An actual nonempty feasible facility set, encoded by its membership mask.

   Also declared: ComparatorChallenges/KMedianThreshold.lean:88 (same declaration text).

   def FactorCorrect (α : ℝ) (I : Instance) (output : List Bool) : Prop :=
   …

   Mentions: OAI.MetricKMedian.Instance

10. def OAI.MetricKMedian.approximationFactors line 40

    Source documentation

    Deterministic polynomial-time approximation factors for arbitrary specified clients and facilities.

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

    def approximationFactors : Set ℝ := {α | ∃ algorithm : Instance → List Bool,
    …

    Mentions: OAI.MetricKMedian.Instance