OAI/Combinatorics/KMedian/Expanders/Rademacher.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedian.PCP.Rademacher.expect_apply line 17
  2. def OAI.MetricKMedian.PCP.Rademacher.wordSum line 26
  3. def OAI.MetricKMedian.PCP.Rademacher.moment line 27
  4. lemma OAI.MetricKMedian.PCP.Rademacher.wordSum_cons line 30
  5. lemma OAI.MetricKMedian.PCP.Rademacher.moment_succ line 36
  6. lemma OAI.MetricKMedian.PCP.Rademacher.moment2_succ line 45
  7. lemma OAI.MetricKMedian.PCP.Rademacher.moment4_succ line 52
  8. lemma OAI.MetricKMedian.PCP.Rademacher.moment6_succ line 59
  9. lemma OAI.MetricKMedian.PCP.Rademacher.moment8_succ line 66
  10. lemma OAI.MetricKMedian.PCP.Rademacher.moment10_succ line 73
  11. theorem OAI.MetricKMedian.PCP.Rademacher.moments_bound line 82
  12. theorem OAI.MetricKMedian.PCP.Rademacher.large_sum_rate line 106