OAI/Combinatorics/KMedianRecovery/Recovery/LeafOrder.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.MetricKMedianRecovery.RationalLeaves.labelLinearOrder line 8
  2. def OAI.MetricKMedianRecovery.CanonicalSensitiveEndpoint.run line 17
  3. lemma OAI.MetricKMedianRecovery.CanonicalSensitiveEndpoint.run_spec line 36
  4. inductive OAI.MetricKMedianRecovery.CanonicalCoupledMerge.Correction line 68
  5. def OAI.MetricKMedianRecovery.CanonicalCoupledMerge.Correction.apply line 72
  6. def OAI.MetricKMedianRecovery.CanonicalCoupledMerge.Correction.error line 76
  7. structure OAI.MetricKMedianRecovery.CanonicalCoupledMerge.State line 80
  8. def OAI.MetricKMedianRecovery.CanonicalCoupledMerge.State.mapPrefix line 89
  9. def OAI.MetricKMedianRecovery.CanonicalCoupledMerge.State.mapFree line 90
  10. def OAI.MetricKMedianRecovery.CanonicalCoupledMerge.State.a line 92
  11. def OAI.MetricKMedianRecovery.CanonicalCoupledMerge.State.b line 95
  12. structure OAI.MetricKMedianRecovery.CanonicalCoupledMerge.Output line 98
  13. structure OAI.MetricKMedianRecovery.CanonicalCoupledMerge.Certified line 106
  14. def OAI.MetricKMedianRecovery.CanonicalCoupledMerge.Certified.coupled line 128
  15. lemma OAI.MetricKMedianRecovery.CanonicalCoupledMerge.Certified.zero_false line 155
  16. def OAI.MetricKMedianRecovery.CanonicalCoupledMerge.Output.Correct line 159