OAI/Combinatorics/KMedianRecovery/Recovery/Average.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.FiniteSampling.average line 10
  2. def OAI.MetricKMedianRecovery.FiniteSampling.probability line 13
  3. def OAI.MetricKMedianRecovery.FiniteSampling.sampleMean line 17
  4. lemma OAI.MetricKMedianRecovery.FiniteSampling.average_congr line 23
  5. lemma OAI.MetricKMedianRecovery.FiniteSampling.average_const line 26
  6. lemma OAI.MetricKMedianRecovery.FiniteSampling.average_mono line 29
  7. lemma OAI.MetricKMedianRecovery.FiniteSampling.average_nonneg line 32
  8. lemma OAI.MetricKMedianRecovery.FiniteSampling.average_le line 35
  9. lemma OAI.MetricKMedianRecovery.FiniteSampling.average_add line 38
  10. lemma OAI.MetricKMedianRecovery.FiniteSampling.average_sub line 42
  11. lemma OAI.MetricKMedianRecovery.FiniteSampling.average_mul_const line 46
  12. lemma OAI.MetricKMedianRecovery.FiniteSampling.average_const_mul line 50
  13. lemma OAI.MetricKMedianRecovery.FiniteSampling.average_sum line 54
  14. lemma OAI.MetricKMedianRecovery.FiniteSampling.average_prod line 58
  15. lemma OAI.MetricKMedianRecovery.FiniteSampling.average_equiv line 63
  16. lemma OAI.MetricKMedianRecovery.FiniteSampling.average_pi_apply line 67
  17. lemma OAI.MetricKMedianRecovery.FiniteSampling.average_pi_mul line 74
  18. lemma OAI.MetricKMedianRecovery.FiniteSampling.variance_identity line 84
  19. lemma OAI.MetricKMedianRecovery.FiniteSampling.bounded_variance line 90
  20. lemma OAI.MetricKMedianRecovery.FiniteSampling.sum_square line 101
  21. lemma OAI.MetricKMedianRecovery.FiniteSampling.variance_sum_pi line 106
  22. lemma OAI.MetricKMedianRecovery.FiniteSampling.sampleMean_variance line 123
  23. lemma OAI.MetricKMedianRecovery.FiniteSampling.probability_nonneg line 141
  24. lemma OAI.MetricKMedianRecovery.FiniteSampling.probability_le_one line 147
  25. lemma OAI.MetricKMedianRecovery.FiniteSampling.probability_mono line 153
  26. lemma OAI.MetricKMedianRecovery.FiniteSampling.probability_false line 161
  27. lemma OAI.MetricKMedianRecovery.FiniteSampling.probability_compl line 165
  28. lemma OAI.MetricKMedianRecovery.FiniteSampling.probability_union line 173
  29. lemma OAI.MetricKMedianRecovery.FiniteSampling.probability_chebyshev line 182
  30. theorem OAI.MetricKMedianRecovery.FiniteSampling.sampleMean_error line 198
  31. lemma OAI.MetricKMedianRecovery.FiniteSampling.probability_congr line 211
  32. lemma OAI.MetricKMedianRecovery.FiniteSampling.probability_pi_apply line 218
  33. lemma OAI.MetricKMedianRecovery.FiniteSampling.probability_exists line 224
  34. theorem OAI.MetricKMedianRecovery.FiniteSampling.simultaneous_sample_error line 246
  35. theorem OAI.MetricKMedianRecovery.FiniteSampling.categorical_batch_error line 264
  36. lemma OAI.MetricKMedianRecovery.FiniteSampling.average_fin_succ line 287
  37. def OAI.MetricKMedianRecovery.FiniteSampling.adaptiveBad line 297
  38. theorem OAI.MetricKMedianRecovery.FiniteSampling.adaptive_union_bound line 302
  39. theorem OAI.MetricKMedianRecovery.FiniteSampling.adaptive_categorical_error line 333
  40. lemma OAI.MetricKMedianRecovery.FiniteSampling.average_on_good line 351