OAI/Combinatorics/KMedianRecovery/Recovery/Table.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedianRecovery.Categorical.Table line 13
  2. def OAI.MetricKMedianRecovery.Categorical.tableWeights line 15
  3. lemma OAI.MetricKMedianRecovery.Categorical.average_option line 19
  4. lemma OAI.MetricKMedianRecovery.Categorical.tableWeights_total line 37
  5. lemma OAI.MetricKMedianRecovery.Categorical.tableWeights_valid line 42
  6. lemma OAI.MetricKMedianRecovery.Categorical.table_operator line 48
  7. lemma OAI.MetricKMedianRecovery.Categorical.average_update line 58
  8. lemma OAI.MetricKMedianRecovery.Categorical.tableWeights_update line 70
  9. lemma OAI.MetricKMedianRecovery.Categorical.average_comm line 94
  10. def OAI.MetricKMedianRecovery.Categorical.put line 98
  11. def OAI.MetricKMedianRecovery.Categorical.draw line 101
  12. def OAI.MetricKMedianRecovery.Categorical.batch line 105
  13. lemma OAI.MetricKMedianRecovery.Categorical.batch_cons line 109
  14. lemma OAI.MetricKMedianRecovery.Categorical.average_draw line 113
  15. lemma OAI.MetricKMedianRecovery.Categorical.mem_draw line 133
  16. lemma OAI.MetricKMedianRecovery.Categorical.batch_valid line 149
  17. lemma OAI.MetricKMedianRecovery.Categorical.batch_length line 156
  18. lemma OAI.MetricKMedianRecovery.Categorical.operator_zero line 159
  19. lemma OAI.MetricKMedianRecovery.Categorical.tableWeights_none line 164
  20. lemma OAI.MetricKMedianRecovery.Categorical.batch_sameweights line 170
  21. def OAI.MetricKMedianRecovery.Categorical.derivative line 178
  22. lemma OAI.MetricKMedianRecovery.Categorical.partial_choice line 183
  23. lemma OAI.MetricKMedianRecovery.Categorical.partial_sample line 188
  24. lemma OAI.MetricKMedianRecovery.Categorical.partial_zero line 195
  25. lemma OAI.MetricKMedianRecovery.Categorical.partial_succ line 207
  26. lemma OAI.MetricKMedianRecovery.Categorical.direction_sum line 226