OAI/Combinatorics/KMedianRecovery/Sampling/RationalSampling.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MetricKMedianRecovery.RationalSampling.State line 9
  2. def OAI.MetricKMedianRecovery.RationalSampling.State.real line 12
  3. def OAI.MetricKMedianRecovery.RationalSampling.tagId line 14
  4. lemma OAI.MetricKMedianRecovery.RationalSampling.tagId_le_iff line 17
  5. lemma OAI.MetricKMedianRecovery.RationalSampling.tagId_injective line 36
  6. def OAI.MetricKMedianRecovery.RationalSampling.tagDistance line 39
  7. lemma OAI.MetricKMedianRecovery.RationalSampling.tagDistance_cast line 49
  8. def OAI.MetricKMedianRecovery.RationalSampling.key line 59
  9. lemma OAI.MetricKMedianRecovery.RationalSampling.key_le_iff line 62
  10. def OAI.MetricKMedianRecovery.RationalSampling.keys line 67
  11. lemma OAI.MetricKMedianRecovery.RationalSampling.keys_nonempty line 70
  12. lemma OAI.MetricKMedianRecovery.RationalSampling.minimum_key line 73
  13. lemma OAI.MetricKMedianRecovery.RationalSampling.minimum_reference line 82