OAI/Combinatorics/KMedianRecovery/Recovery/LeafOutcome.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.PhaseSensitiveCrossing.LeafOutcome line 11
  2. theorem OAI.MetricKMedianRecovery.PhaseSensitiveCrossing.sensitive_search line 19
  3. theorem OAI.MetricKMedianRecovery.PhaseSensitiveCrossing.three_free_phase line 60
  4. def OAI.MetricKMedianRecovery.PhaseFreshAllocation.incl line 80
  5. def OAI.MetricKMedianRecovery.PhaseFreshAllocation.enlargedMetric line 83
  6. def OAI.MetricKMedianRecovery.PhaseFreshAllocation.copy line 86
  7. lemma OAI.MetricKMedianRecovery.PhaseFreshAllocation.original_dist line 90
  8. lemma OAI.MetricKMedianRecovery.PhaseFreshAllocation.copy_dist line 96
  9. lemma OAI.MetricKMedianRecovery.PhaseFreshAllocation.copy_fresh line 104
  10. lemma OAI.MetricKMedianRecovery.PhaseFreshAllocation.spare_fresh line 110
  11. lemma OAI.MetricKMedianRecovery.PhaseFreshAllocation.disjoint_image line 117
  12. theorem OAI.MetricKMedianRecovery.PhaseFreshAllocation.allocated_crossing line 125