OAI/Combinatorics/KMedianRecovery/Recovery/InitialState2.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.Categorical.initialState line 9
  2. lemma OAI.MetricKMedianRecovery.Categorical.initialState_invariant line 12
  3. lemma OAI.MetricKMedianRecovery.Categorical.draw_none line 21
  4. lemma OAI.MetricKMedianRecovery.Categorical.tableValue_none line 27
  5. def OAI.MetricKMedianRecovery.Categorical.greedyRun line 37
  6. def OAI.MetricKMedianRecovery.Categorical.greedyOutput line 41
  7. lemma OAI.MetricKMedianRecovery.Categorical.greedyRun_invariant line 45
  8. lemma OAI.MetricKMedianRecovery.Categorical.greedyOutput_feasible line 51
  9. lemma OAI.MetricKMedianRecovery.Categorical.greedyRun_expectation line 57
  10. lemma OAI.MetricKMedianRecovery.Categorical.tableValue_nonneg line 66
  11. lemma OAI.MetricKMedianRecovery.Categorical.greedyRun_good line 73