OAI/Combinatorics/KMedianRecovery/Geometry/LocalIndex.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedianRecovery.Sampling.LocalIndex line 12
  2. abbrev OAI.MetricKMedianRecovery.Sampling.LocalJoint line 15
  3. def OAI.MetricKMedianRecovery.Sampling.localTapeEquiv line 18
  4. def OAI.MetricKMedianRecovery.Sampling.localTapeBound line 28
  5. lemma OAI.MetricKMedianRecovery.Sampling.localIndex_card_le line 32
  6. def OAI.MetricKMedianRecovery.Sampling.localEmbedding line 45
  7. def OAI.MetricKMedianRecovery.Sampling.branchJointOutput line 50
  8. def OAI.MetricKMedianRecovery.Sampling.branchTapeOutput line 60
  9. lemma OAI.MetricKMedianRecovery.Sampling.branchJointOutput_feasible line 68
  10. lemma OAI.MetricKMedianRecovery.Sampling.branchTapeOutput_feasible line 86
  11. lemma OAI.MetricKMedianRecovery.Sampling.localTape_probability line 95
  12. lemma OAI.MetricKMedianRecovery.Sampling.branchTape_probability line 103