OAI/Combinatorics/ThinTrees/Encoding/GraphRealization.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

Graph realization.

  1. structure OAI.AlgorithmicThinTrees.GraphStack.Graph line 17
  2. abbrev OAI.AlgorithmicThinTrees.GraphStack.graphDataCode line 22
  3. def OAI.AlgorithmicThinTrees.GraphStack.Graph.data line 23
  4. def OAI.AlgorithmicThinTrees.GraphStack.graphCode line 25
  5. abbrev OAI.AlgorithmicThinTrees.GraphStack.view line 26
  6. instance OAI.AlgorithmicThinTrees.GraphStack.poly_view line 28
  7. abbrev OAI.AlgorithmicThinTrees.GraphStack.numVertices line 32
  8. abbrev OAI.AlgorithmicThinTrees.GraphStack.endpoints line 33
  9. abbrev OAI.AlgorithmicThinTrees.GraphStack.lefts line 34
  10. abbrev OAI.AlgorithmicThinTrees.GraphStack.rights line 35
  11. def OAI.AlgorithmicThinTrees.GraphStack.numEdges line 36
  12. instance OAI.AlgorithmicThinTrees.GraphStack.poly_numEdges line 38
  13. abbrev OAI.AlgorithmicThinTrees.GraphStack.Edge line 40
  14. abbrev OAI.AlgorithmicThinTrees.GraphStack.edgeCode line 41
  15. abbrev OAI.AlgorithmicThinTrees.GraphStack.edgeGraph line 42
  16. abbrev OAI.AlgorithmicThinTrees.GraphStack.edgeIndex line 43
  17. def OAI.AlgorithmicThinTrees.GraphStack.edgeLeft line 45
  18. def OAI.AlgorithmicThinTrees.GraphStack.edgeRight line 48
  19. instance OAI.AlgorithmicThinTrees.GraphStack.poly_edgeLeft line 51
  20. instance OAI.AlgorithmicThinTrees.GraphStack.poly_edgeRight line 52
  21. def OAI.AlgorithmicThinTrees.GraphStack.incidence line 54
  22. instance OAI.AlgorithmicThinTrees.GraphStack.poly_incidence line 66
  23. def OAI.AlgorithmicThinTrees.GraphStack.incidenceRows line 68
  24. instance OAI.AlgorithmicThinTrees.GraphStack.poly_incidenceRows line 71
  25. def OAI.AlgorithmicThinTrees.GraphStack.laplacian line 73
  26. instance OAI.AlgorithmicThinTrees.GraphStack.poly_laplacian line 87
  27. def OAI.AlgorithmicThinTrees.GraphStack.constantMatrix line 89
  28. instance OAI.AlgorithmicThinTrees.GraphStack.poly_constantMatrix line 98
  29. def OAI.AlgorithmicThinTrees.GraphStack.projection line 100
  30. instance OAI.AlgorithmicThinTrees.GraphStack.poly_projection line 108
  31. def OAI.AlgorithmicThinTrees.GraphStack.response line 110
  32. instance OAI.AlgorithmicThinTrees.GraphStack.poly_response line 124
  33. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.matIndex_val line 132
  34. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.mulIndex_val line 133
  35. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.edgeIndex_val line 135
  36. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.flowIndex_val line 137
  37. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.dimsCode line 140
  38. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.variablesCode line 141
  39. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.variablesDims line 142
  40. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.variablesN line 143
  41. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.variablesM line 144
  42. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.variableValues line 145
  43. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.dimensionProgram line 147
  44. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_dimensionProgram line 153
  45. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.varEntryCode line 157
  46. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.varEntryContext line 158
  47. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.varEntryVars line 159
  48. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.varEntryI line 160
  49. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.varEntryJ line 161
  50. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.rawEntry line 163
  51. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_rawEntry line 167
  52. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.raw line 169
  53. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_raw line 173
  54. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.raw_data line 175
  55. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.edgeVariable line 186
  56. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_edgeVariable line 196
  57. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.edgeVariable_data line 198