OAI/Combinatorics/KMedianRecovery/Recovery/TableValue.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.Categorical.tableValue line 10
  2. abbrev OAI.MetricKMedianRecovery.Categorical.GreedyState line 17
  3. abbrev OAI.MetricKMedianRecovery.Categorical.OracleSeed line 18
  4. def OAI.MetricKMedianRecovery.Categorical.marginalSample line 20
  5. def OAI.MetricKMedianRecovery.Categorical.scores line 24
  6. def OAI.MetricKMedianRecovery.Categorical.greedyStep line 28
  7. def OAI.MetricKMedianRecovery.Categorical.GreedyInvariant line 35
  8. lemma OAI.MetricKMedianRecovery.Categorical.greedyStep_clock line 39
  9. lemma OAI.MetricKMedianRecovery.Categorical.greedyStep_invariant line 44
  10. lemma OAI.MetricKMedianRecovery.Categorical.draw_feasible line 69
  11. lemma OAI.MetricKMedianRecovery.Categorical.marginalSample_average line 83
  12. lemma OAI.MetricKMedianRecovery.Categorical.sampled_select_choice line 88
  13. lemma OAI.MetricKMedianRecovery.Categorical.tableValue_eq line 111
  14. lemma OAI.MetricKMedianRecovery.Categorical.advance_gain line 114
  15. lemma OAI.MetricKMedianRecovery.Categorical.advance_recurrence line 133
  16. def OAI.MetricKMedianRecovery.Categorical.estimationBad line 160
  17. lemma OAI.MetricKMedianRecovery.Categorical.greedyStep_recurrence line 164
  18. lemma OAI.MetricKMedianRecovery.Categorical.greedy_failure_bound line 181