OAI/Combinatorics/KMedian/Projection/Seed.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.PCP.BiProjection.neutral line 20
  2. lemma OAI.MetricKMedian.PCP.BiProjection.neutral_perfect line 23
  3. lemma OAI.MetricKMedian.PCP.BiProjection.neutral_consistent line 26
  4. lemma OAI.MetricKMedian.PCP.BiProjection.collisionBound_mono line 32
  5. def OAI.MetricKMedian.PCP.ProjectionSeed.gap line 40
  6. lemma OAI.MetricKMedian.PCP.ProjectionSeed.gap_pos line 41
  7. lemma OAI.MetricKMedian.PCP.ProjectionSeed.gap_le_one line 46
  8. def OAI.MetricKMedian.PCP.ProjectionSeed.contraction line 51
  9. lemma OAI.MetricKMedian.PCP.ProjectionSeed.contraction_nonneg line 52
  10. lemma OAI.MetricKMedian.PCP.ProjectionSeed.contraction_lt_one line 53
  11. abbrev OAI.MetricKMedian.PCP.ProjectionSeed.Degree line 60
  12. abbrev OAI.MetricKMedian.PCP.ProjectionSeed.Port line 61
  13. abbrev OAI.MetricKMedian.PCP.ProjectionSeed.LeftLabel line 62
  14. abbrev OAI.MetricKMedian.PCP.ProjectionSeed.RightLabel line 63
  15. abbrev OAI.MetricKMedian.PCP.ProjectionSeed.LeftPort line 64
  16. abbrev OAI.MetricKMedian.PCP.ProjectionSeed.Node line 66
  17. def OAI.MetricKMedian.PCP.ProjectionSeed.csp line 67
  18. instance OAI.MetricKMedian.PCP.ProjectionSeed.nodeNonempty line 68
  19. lemma OAI.MetricKMedian.PCP.ProjectionSeed.rejection line 70
  20. def OAI.MetricKMedian.PCP.ProjectionSeed.HasLegal line 81
  21. def OAI.MetricKMedian.PCP.ProjectionSeed.chosen line 82
  22. lemma OAI.MetricKMedian.PCP.ProjectionSeed.chosen_legal line 83
  23. def OAI.MetricKMedian.PCP.ProjectionSeed.good line 84
  24. def OAI.MetricKMedian.PCP.ProjectionSeed.bad line 87
  25. lemma OAI.MetricKMedian.PCP.ProjectionSeed.good_consistent line 89
  26. lemma OAI.MetricKMedian.PCP.ProjectionSeed.bad_consistent line 92
  27. lemma OAI.MetricKMedian.PCP.ProjectionSeed.hasLegal_of_perfect line 94
  28. lemma OAI.MetricKMedian.PCP.ProjectionSeed.good_perfect line 100
  29. lemma OAI.MetricKMedian.PCP.ProjectionSeed.good_bound line 105
  30. lemma OAI.MetricKMedian.PCP.ProjectionSeed.bad_bound line 118