OAI/Combinatorics/KMedianRecovery/Refined/Bounds.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Explicit charge coefficients, finite probability bounds, and conditional extraction.

  1. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Analysis.inverse_e_lt_half line 9
  2. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Analysis.third_lt_inverse_e line 13
  3. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Analysis.rational_theta line 17
  4. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Analysis.cube_div_q line 25
  5. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Analysis.quadratic_cubic_error line 29
  6. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Analysis.explicit_coefficient line 37
  7. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Analysis.sum_five_charges line 47
  8. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Analysis.expectation_slack line 105
  9. def OAI.MetricKMedianRecovery.RefinedRecovery.Analysis.finiteAverage line 110
  10. def OAI.MetricKMedianRecovery.RefinedRecovery.Analysis.finiteProbability line 113
  11. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Analysis.finite_markov line 117
  12. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Analysis.conditional_extraction line 144