OAI/Combinatorics/KMedian/Expanders/CloudPrograms.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.MetricKMedian.PCP.Compiler.unitHardcoded line 12
  2. instance OAI.MetricKMedian.PCP.Compiler.boolHardcoded line 14
  3. abbrev OAI.MetricKMedian.PCP.Compiler.CloudProgram.Dart line 19
  4. def OAI.MetricKMedian.PCP.Compiler.CloudProgram.darts line 20
  5. def OAI.MetricKMedian.PCP.Compiler.CloudProgram.endpoint line 22
  6. def OAI.MetricKMedian.PCP.Compiler.CloudProgram.incident line 24
  7. def OAI.MetricKMedian.PCP.Compiler.CloudProgram.active line 26
  8. def OAI.MetricKMedian.PCP.Compiler.CloudProgram.cloud line 28
  9. def OAI.MetricKMedian.PCP.Compiler.CloudProgram.nodes line 30
  10. def OAI.MetricKMedian.PCP.Compiler.CloudProgram.global line 32
  11. def OAI.MetricKMedian.PCP.Compiler.CloudProgram.index line 34
  12. def OAI.MetricKMedian.PCP.Compiler.CloudProgram.dartIndex line 36
  13. lemma OAI.MetricKMedian.PCP.Compiler.CloudProgram.poly_darts line 38
  14. lemma OAI.MetricKMedian.PCP.Compiler.CloudProgram.poly_endpoint line 43
  15. lemma OAI.MetricKMedian.PCP.Compiler.CloudProgram.poly_incident line 47
  16. lemma OAI.MetricKMedian.PCP.Compiler.CloudProgram.poly_active line 52
  17. lemma OAI.MetricKMedian.PCP.Compiler.CloudProgram.poly_cloud line 57
  18. lemma OAI.MetricKMedian.PCP.Compiler.CloudProgram.poly_nodes line 63
  19. lemma OAI.MetricKMedian.PCP.Compiler.CloudProgram.poly_global line 70
  20. lemma OAI.MetricKMedian.PCP.Compiler.CloudProgram.poly_index line 76
  21. lemma OAI.MetricKMedian.PCP.Compiler.CloudProgram.poly_dartIndex line 83