OAI/Combinatorics/KMedianRecovery/Encoding/RationalMenus.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.RationalSampling.leafValues line 11
  2. def OAI.MetricKMedianRecovery.RationalSampling.nearestLeaf line 13
  3. def OAI.MetricKMedianRecovery.RationalSampling.menuWeight line 15
  4. lemma OAI.MetricKMedianRecovery.RationalSampling.menuWeight_cast line 19
  5. lemma OAI.MetricKMedianRecovery.RationalSampling.leaves_empty_iff line 28
  6. lemma OAI.MetricKMedianRecovery.RationalSampling.leafValues_nonempty line 30
  7. lemma OAI.MetricKMedianRecovery.RationalSampling.nearestLeaf_cast line 32
  8. def OAI.MetricKMedianRecovery.RationalSampling.menuRadius line 55
  9. lemma OAI.MetricKMedianRecovery.RationalSampling.menuRadius_cast line 60
  10. def OAI.MetricKMedianRecovery.RationalSampling.chosenKey line 77
  11. def OAI.MetricKMedianRecovery.RationalSampling.reference line 79
  12. def OAI.MetricKMedianRecovery.RationalSampling.chosenId line 81
  13. def OAI.MetricKMedianRecovery.RationalSampling.clientWeight line 83
  14. def OAI.MetricKMedianRecovery.RationalSampling.totalWeight line 85
  15. def OAI.MetricKMedianRecovery.RationalSampling.transitionWeight line 87
  16. def OAI.MetricKMedianRecovery.RationalSampling.State.remove line 97
  17. def OAI.MetricKMedianRecovery.RationalSampling.State.add line 98
  18. def OAI.MetricKMedianRecovery.RationalSampling.retain line 99
  19. lemma OAI.MetricKMedianRecovery.RationalSampling.remove_real line 101
  20. lemma OAI.MetricKMedianRecovery.RationalSampling.add_real line 106
  21. lemma OAI.MetricKMedianRecovery.RationalSampling.retain_real line 108
  22. def OAI.MetricKMedianRecovery.RationalSampling.update line 111
  23. lemma OAI.MetricKMedianRecovery.RationalSampling.reference_cast line 126
  24. lemma OAI.MetricKMedianRecovery.RationalSampling.chosenId_eq line 128
  25. lemma OAI.MetricKMedianRecovery.RationalSampling.clientWeight_cast line 131
  26. lemma OAI.MetricKMedianRecovery.RationalSampling.totalWeight_cast line 134
  27. lemma OAI.MetricKMedianRecovery.RationalSampling.transitionWeight_cast line 137
  28. lemma OAI.MetricKMedianRecovery.RationalSampling.update_real line 150