OAI/Combinatorics/KMedianRecovery/Refined/Model.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Normalized metric inputs, hidden comparison certificates, and the refined recovery claim.

  1. structure OAI.MetricKMedianRecovery.RefinedRecovery.Input line 9

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

  2. abbrev OAI.MetricKMedianRecovery.RefinedRecovery.Input.Point line 19

    Also declared: ComparatorChallenges/KMedianRefinedRecovery.lean:75 (same declaration text).

  3. def OAI.MetricKMedianRecovery.RefinedRecovery.Input.size line 21

    Also declared: ComparatorChallenges/KMedianRefinedRecovery.lean:77 (same declaration text).

  4. def OAI.MetricKMedianRecovery.RefinedRecovery.Input.Bounded line 23

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

  5. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Input.anchor_nonempty line 26
  6. def OAI.MetricKMedianRecovery.RefinedRecovery.Input.assign line 29

    Also declared: ComparatorChallenges/KMedianRefinedRecovery.lean:82 (same declaration text).

  7. def OAI.MetricKMedianRecovery.RefinedRecovery.Input.cluster line 35

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

  8. def OAI.MetricKMedianRecovery.RefinedRecovery.Input.clusterCost line 38

    Also declared: ComparatorChallenges/KMedianRefinedRecovery.lean:91 (same declaration text).

  9. def OAI.MetricKMedianRecovery.RefinedRecovery.Input.anchorBits line 41

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

  10. structure OAI.MetricKMedianRecovery.RefinedRecovery.Certificate line 46

    Also declared: ComparatorChallenges/KMedianRefinedRecovery.lean:99 (same declaration text).

  11. def OAI.MetricKMedianRecovery.RefinedRecovery.Certificate.bad line 63
  12. def OAI.MetricKMedianRecovery.RefinedRecovery.Certificate.nonproxy line 64
  13. def OAI.MetricKMedianRecovery.RefinedRecovery.precision line 68

    Also declared: ComparatorChallenges/KMedianRefinedRecovery.lean:114 (same declaration text).

  14. def OAI.MetricKMedianRecovery.RefinedRecovery.queryBits line 71

    Also declared: ComparatorChallenges/KMedianRefinedRecovery.lean:117 (same declaration text).

  15. def OAI.MetricKMedianRecovery.RefinedRecovery.seedLength line 74

    Also declared: ComparatorChallenges/KMedianRefinedRecovery.lean:120 (same declaration text).

  16. abbrev OAI.MetricKMedianRecovery.RefinedRecovery.Seed line 77

    Also declared: ComparatorChallenges/KMedianRefinedRecovery.lean:123 (same declaration text).

  17. def OAI.MetricKMedianRecovery.RefinedRecovery.output line 80

    Also declared: ComparatorChallenges/KMedianRefinedRecovery.lean:126 (same declaration text).

  18. def OAI.MetricKMedianRecovery.RefinedRecovery.successProbability line 84

    Also declared: ComparatorChallenges/KMedianRefinedRecovery.lean:130 (same declaration text).

  19. def OAI.MetricKMedianRecovery.RefinedRecovery.workBound line 91

    Also declared: ComparatorChallenges/KMedianRefinedRecovery.lean:137 (same declaration text).

  20. def OAI.MetricKMedianRecovery.RefinedRecovery.PolynomialWork line 96

    Also declared: ComparatorChallenges/KMedianRefinedRecovery.lean:142 (same declaration text).

  21. def OAI.MetricKMedianRecovery.RefinedRecovery.refinedRecoveryClaim line 102