OAI/Combinatorics/KMedianRecovery/Recovery/SetFunction.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedianRecovery.Categorical.SetFunction line 11
  2. def OAI.MetricKMedianRecovery.Categorical.marginal line 13
  3. def OAI.MetricKMedianRecovery.Categorical.operator line 16
  4. def OAI.MetricKMedianRecovery.Categorical.IsWeight line 19
  5. abbrev OAI.MetricKMedianRecovery.Categorical.Batch line 21
  6. def OAI.MetricKMedianRecovery.Categorical.evaluate line 23
  7. def OAI.MetricKMedianRecovery.Categorical.direction line 27
  8. def OAI.MetricKMedianRecovery.Categorical.addMass line 31
  9. def OAI.MetricKMedianRecovery.Categorical.update line 34
  10. def OAI.MetricKMedianRecovery.Categorical.HasRoom line 37
  11. def OAI.MetricKMedianRecovery.Categorical.BoundedMarginals line 40
  12. lemma OAI.MetricKMedianRecovery.Categorical.operator_const line 43
  13. lemma OAI.MetricKMedianRecovery.Categorical.operator_add line 48
  14. lemma OAI.MetricKMedianRecovery.Categorical.operator_smul line 53
  15. lemma OAI.MetricKMedianRecovery.Categorical.operator_sub line 64
  16. lemma OAI.MetricKMedianRecovery.Categorical.operator_mono line 69
  17. lemma OAI.MetricKMedianRecovery.Categorical.operator_bounds line 75
  18. lemma OAI.MetricKMedianRecovery.Categorical.marginal_operator line 82
  19. lemma OAI.MetricKMedianRecovery.Categorical.operator_marginals line 94
  20. lemma OAI.MetricKMedianRecovery.Categorical.sum_addMass line 100
  21. lemma OAI.MetricKMedianRecovery.Categorical.addMass_weight line 104
  22. lemma OAI.MetricKMedianRecovery.Categorical.operator_addMass line 112
  23. lemma OAI.MetricKMedianRecovery.Categorical.evaluate_add line 124
  24. lemma OAI.MetricKMedianRecovery.Categorical.evaluate_smul line 134
  25. lemma OAI.MetricKMedianRecovery.Categorical.evaluate_const line 144
  26. lemma OAI.MetricKMedianRecovery.Categorical.evaluate_mono line 154
  27. lemma OAI.MetricKMedianRecovery.Categorical.evaluate_bounds line 164
  28. lemma OAI.MetricKMedianRecovery.Categorical.evaluate_addMass_head line 171
  29. lemma OAI.MetricKMedianRecovery.Categorical.update_weights line 179
  30. lemma OAI.MetricKMedianRecovery.Categorical.evaluate_update_lower line 185
  31. theorem OAI.MetricKMedianRecovery.Categorical.categorical_update_bound line 208
  32. def OAI.MetricKMedianRecovery.Categorical.Diminishing line 229
  33. lemma OAI.MetricKMedianRecovery.Categorical.boundedMarginals_of_submodular line 233
  34. def OAI.MetricKMedianRecovery.Categorical.allMarginals line 243
  35. def OAI.MetricKMedianRecovery.Categorical.choices line 247
  36. lemma OAI.MetricKMedianRecovery.Categorical.submodular_telescope line 252
  37. lemma OAI.MetricKMedianRecovery.Categorical.comparison_gap line 264
  38. lemma OAI.MetricKMedianRecovery.Categorical.operator_diminishing line 271
  39. lemma OAI.MetricKMedianRecovery.Categorical.operator_le_self line 283
  40. lemma OAI.MetricKMedianRecovery.Categorical.operator_marginal_le line 292
  41. lemma OAI.MetricKMedianRecovery.Categorical.operator_allMarginals line 299
  42. lemma OAI.MetricKMedianRecovery.Categorical.direction_dominates line 307
  43. lemma OAI.MetricKMedianRecovery.Categorical.evaluate_sub line 327
  44. theorem OAI.MetricKMedianRecovery.Categorical.categorical_comparison_direction line 335
  45. def OAI.MetricKMedianRecovery.Categorical.SameWeights line 343
  46. lemma OAI.MetricKMedianRecovery.Categorical.evaluate_eq_of_sameWeights line 345
  47. def OAI.MetricKMedianRecovery.Categorical.ChoiceErrors line 356
  48. lemma OAI.MetricKMedianRecovery.Categorical.choiceErrors_weights line 363