OAI/Combinatorics/KMedian/Amplification/FlexibleCloud.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.PCP.FlexibleCloud.dartEmbed line 17
  2. def OAI.MetricKMedian.PCP.FlexibleCloud.matchingGraph line 30
  3. def OAI.MetricKMedian.PCP.FlexibleCloud.matchingCSP line 31
  4. lemma OAI.MetricKMedian.PCP.FlexibleCloud.matching_bad line 34
  5. abbrev OAI.MetricKMedian.PCP.FlexibleCloud.RegularPort line 41
  6. def OAI.MetricKMedian.PCP.FlexibleCloud.regularGraph line 42
  7. def OAI.MetricKMedian.PCP.FlexibleCloud.regularCSP line 43
  8. lemma OAI.MetricKMedian.PCP.FlexibleCloud.honest_dart line 46
  9. lemma OAI.MetricKMedian.PCP.FlexibleCloud.matching_complete line 50
  10. lemma OAI.MetricKMedian.PCP.FlexibleCloud.regular_complete line 66
  11. lemma OAI.MetricKMedian.PCP.FlexibleCloud.edge_bad_cases line 73
  12. lemma OAI.MetricKMedian.PCP.FlexibleCloud.old_raw line 89
  13. lemma OAI.MetricKMedian.PCP.FlexibleCloud.matching_sum_bound line 107
  14. theorem OAI.MetricKMedian.PCP.FlexibleCloud.regular_sound line 118