OAI/Combinatorics/KMedianRecovery/Geometry/LeafDistances.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.Sampling.leafDistances line 13
  2. def OAI.MetricKMedianRecovery.Sampling.nearestLeaf line 16
  3. lemma OAI.MetricKMedianRecovery.Sampling.nearestLeaf_of_mem line 19
  4. lemma OAI.MetricKMedianRecovery.Sampling.nearestLeaf_lower line 28
  5. abbrev OAI.MetricKMedianRecovery.Sampling.Entry line 39
  6. abbrev OAI.MetricKMedianRecovery.Sampling.Action line 40
  7. def OAI.MetricKMedianRecovery.Sampling.clientWeight line 42
  8. def OAI.MetricKMedianRecovery.Sampling.totalWeight line 45
  9. lemma OAI.MetricKMedianRecovery.Sampling.clientWeight_nonneg line 48
  10. lemma OAI.MetricKMedianRecovery.Sampling.clientWeight_eq line 51
  11. lemma OAI.MetricKMedianRecovery.Sampling.menuWeight_nonneg line 56
  12. def OAI.MetricKMedianRecovery.Sampling.transitionWeight line 65
  13. lemma OAI.MetricKMedianRecovery.Sampling.transitionWeight_nonneg line 76
  14. lemma OAI.MetricKMedianRecovery.Sampling.transitionWeight_total line 92
  15. def OAI.MetricKMedianRecovery.Sampling.actualKernel line 109
  16. def OAI.MetricKMedianRecovery.Sampling.menuRadius line 114
  17. def OAI.MetricKMedianRecovery.Sampling.retain line 120
  18. def OAI.MetricKMedianRecovery.Sampling.update line 123
  19. lemma OAI.MetricKMedianRecovery.Sampling.retained_limits line 142
  20. lemma OAI.MetricKMedianRecovery.Sampling.update_limits line 149