OAI/Combinatorics/KMedian/Expanders/CloudCopies.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.PCP.CloudCopies.Dart line 17
  2. def OAI.MetricKMedian.PCP.CloudCopies.endpoint line 19
  3. abbrev OAI.MetricKMedian.PCP.CloudCopies.Active line 20
  4. def OAI.MetricKMedian.PCP.CloudCopies.owner line 21
  5. lemma OAI.MetricKMedian.PCP.CloudCopies.owner_surjective line 24
  6. abbrev OAI.MetricKMedian.PCP.CloudCopies.Incident line 28
  7. instance OAI.MetricKMedian.PCP.CloudCopies.incidentNonempty line 29
  8. def OAI.MetricKMedian.PCP.CloudCopies.depth line 33
  9. abbrev OAI.MetricKMedian.PCP.CloudCopies.Copy line 34
  10. abbrev OAI.MetricKMedian.PCP.CloudCopies.Node line 35
  11. lemma OAI.MetricKMedian.PCP.CloudCopies.copy_card_lower line 38
  12. lemma OAI.MetricKMedian.PCP.CloudCopies.copy_card_upper line 45
  13. def OAI.MetricKMedian.PCP.CloudCopies.incidentEmbed line 52
  14. def OAI.MetricKMedian.PCP.CloudCopies.dartEmbed line 56
  15. lemma OAI.MetricKMedian.PCP.CloudCopies.node_card_upper line 68
  16. instance OAI.MetricKMedian.PCP.CloudCopies.activeNonempty line 79
  17. instance OAI.MetricKMedian.PCP.CloudCopies.nodeNonempty line 82
  18. def OAI.MetricKMedian.PCP.CloudCopies.equalityRotate line 86
  19. lemma OAI.MetricKMedian.PCP.CloudCopies.equalityRotate_involutive line 91
  20. def OAI.MetricKMedian.PCP.CloudCopies.equalityGraph line 95
  21. lemma OAI.MetricKMedian.PCP.CloudCopies.equality_step line 103
  22. def OAI.MetricKMedian.PCP.CloudCopies.decoded line 107
  23. lemma OAI.MetricKMedian.PCP.CloudCopies.decoded_active line 112
  24. theorem OAI.MetricKMedian.PCP.CloudCopies.cloud_sound line 117