OAI/Combinatorics/IndependentSets/Expansion/ExpanderRowControl.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.PCP.ExpanderRowControl.degree line 10
  2. abbrev OAI.IndependentSetsGames.Foundations.PCP.ExpanderRowControl.cloudSize line 11
  3. abbrev OAI.IndependentSetsGames.Foundations.PCP.ExpanderRowControl.rowFactor line 12
  4. structure OAI.IndependentSetsGames.Foundations.PCP.ExpanderRowControl.Control line 14
  5. def OAI.IndependentSetsGames.Foundations.PCP.ExpanderRowControl.squarePorts line 22
  6. def OAI.IndependentSetsGames.Foundations.PCP.ExpanderRowControl.start line 25
  7. def OAI.IndependentSetsGames.Foundations.PCP.ExpanderRowControl.receiveFirst line 36
  8. def OAI.IndependentSetsGames.Foundations.PCP.ExpanderRowControl.receiveSecond line 39
  9. def OAI.IndependentSetsGames.Foundations.PCP.ExpanderRowControl.firstOffset line 46
  10. def OAI.IndependentSetsGames.Foundations.PCP.ExpanderRowControl.secondOffset line 47
  11. def OAI.IndependentSetsGames.Foundations.PCP.ExpanderRowControl.outputPort line 49
  12. def OAI.IndependentSetsGames.Foundations.PCP.ExpanderRowControl.outputOffset line 52
  13. def OAI.IndependentSetsGames.Foundations.PCP.ExpanderRowControl.firstAddress line 55
  14. def OAI.IndependentSetsGames.Foundations.PCP.ExpanderRowControl.secondAddress line 58
  15. def OAI.IndependentSetsGames.Foundations.PCP.ExpanderRowControl.outputAddress line 61
  16. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderRowControl.firstOffset_receiveFirst line 64
  17. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderRowControl.secondOffset_receiveFirst line 67
  18. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderRowControl.receiveFirst_port line 70
  19. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderRowControl.receiveSecond_port line 73
  20. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderRowControl.firstAddress_eq_rowIndex line 76
  21. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderRowControl.secondAddress_eq_rowIndex line 82
  22. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderRowControl.firstAddress_lt line 88
  23. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderRowControl.secondAddress_lt line 93
  24. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderRowControl.lookup_vertex_div line 98
  25. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderRowControl.lookup_port_mod line 101
  26. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderRowControl.lookup_port_eq_remainder line 104
  27. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderRowControl.rowIndex_lookup line 108
  28. def OAI.IndependentSetsGames.Foundations.PCP.ExpanderRowControl.outputPair line 112
  29. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderRowControl.outputAddress_eq_rowIndex line 116
  30. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderRowControl.outputAddress_lt line 122
  31. def OAI.IndependentSetsGames.Foundations.PCP.ExpanderRowControl.evaluateRow line 127
  32. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderRowControl.evaluateRow_eq_lookup_step line 136
  33. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderRowControl.outputAddress_eq_step_row line 145
  34. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderRowControl.outputAddress_eq_step_reverseIndex line 153