OAI/Combinatorics/KMedian/Amplification/Amplifier.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.PCP.Amplifier.Label line 16
  2. abbrev OAI.MetricKMedian.PCP.Amplifier.Degree line 17
  3. def OAI.MetricKMedian.PCP.Amplifier.loss line 18
  4. def OAI.MetricKMedian.PCP.Amplifier.capLoss line 19
  5. def OAI.MetricKMedian.PCP.Amplifier.steps line 20
  6. def OAI.MetricKMedian.PCP.Amplifier.radius line 21
  7. abbrev OAI.MetricKMedian.PCP.Amplifier.Bits line 22
  8. instance OAI.MetricKMedian.PCP.Amplifier.bitsFintype line 23
  9. instance OAI.MetricKMedian.PCP.Amplifier.bitsDecidableEq line 24
  10. instance OAI.MetricKMedian.PCP.Amplifier.edgeSampleFintype line 25
  11. lemma OAI.MetricKMedian.PCP.Amplifier.loss_cast line 27
  12. theorem OAI.MetricKMedian.PCP.Amplifier.loss_pos line 30
  13. theorem OAI.MetricKMedian.PCP.Amplifier.capLoss_pos line 35
  14. theorem OAI.MetricKMedian.PCP.Amplifier.steps_pos line 36
  15. abbrev OAI.MetricKMedian.PCP.Amplifier.Node line 42
  16. abbrev OAI.MetricKMedian.PCP.Amplifier.Edge line 43
  17. instance OAI.MetricKMedian.PCP.Amplifier.nodeFintype line 44
  18. instance OAI.MetricKMedian.PCP.Amplifier.edgeFintype line 45
  19. def OAI.MetricKMedian.PCP.Amplifier.powered line 46
  20. def OAI.MetricKMedian.PCP.Amplifier.bits line 47
  21. abbrev OAI.MetricKMedian.PCP.Amplifier.NewNode line 49
  22. abbrev OAI.MetricKMedian.PCP.Amplifier.NewEdge line 50
  23. instance OAI.MetricKMedian.PCP.Amplifier.newNodeFintype line 51
  24. instance OAI.MetricKMedian.PCP.Amplifier.newEdgeFintype line 52
  25. def OAI.MetricKMedian.PCP.Amplifier.result line 53
  26. def OAI.MetricKMedian.PCP.Amplifier.poweredAssignment line 55
  27. def OAI.MetricKMedian.PCP.Amplifier.decoded line 58
  28. theorem OAI.MetricKMedian.PCP.Amplifier.complete line 62
  29. theorem OAI.MetricKMedian.PCP.Amplifier.sound line 67