OAI/Combinatorics/KMedianRecovery/Branching/CategoricalScore.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.elemBits line 11
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.partBits line 12
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.oracleBits line 13
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.scorePack line 15
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.elementPart line 18
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.elementPart_computes line 20
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.elementSamples line 22
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.elementSamples_computes line 24
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.marginalDraw line 26
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.marginalDraw_computes line 28
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.marginal line 32
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.marginal_computes line 36
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.marginalValues line 41
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.marginalValues_computes line 44
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.score line 47
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.score_computes line 50
  17. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.elementPart_pack line 53
  18. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.elementSamples_pack line 58
  19. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.marginalDraw_pack line 63
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.rationalMarginal line 73
  21. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.marginal_pack line 77
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.rationalScore line 91
  23. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.score_pack line 94
  24. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.rationalScore_cast line 105