OAI/Combinatorics/ThinTrees/Sparsification/Realization.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

Sparsification realization.

  1. def OAI.CurrentKS.Realization.ratNatFloorBinary line 15
  2. instance OAI.CurrentKS.Realization.poly_ratNatFloorBinary line 26
  3. lemma OAI.CurrentKS.Realization.runsPoly_binaryToNat line 29
  4. structure OAI.AlgorithmicThinTrees.GraphicHalf.Stack.Problem line 42
  5. def OAI.AlgorithmicThinTrees.GraphicHalf.Stack.Problem.graph line 48
  6. def OAI.AlgorithmicThinTrees.GraphicHalf.Stack.problemCode line 49
  7. abbrev OAI.AlgorithmicThinTrees.GraphicHalf.Stack.problemView line 50
  8. instance OAI.AlgorithmicThinTrees.GraphicHalf.Stack.poly_problemView line 52
  9. abbrev OAI.AlgorithmicThinTrees.GraphicHalf.Stack.problemGraph line 56
  10. abbrev OAI.AlgorithmicThinTrees.GraphicHalf.Stack.problemCount line 57
  11. abbrev OAI.AlgorithmicThinTrees.GraphicHalf.Stack.problemN line 58
  12. abbrev OAI.AlgorithmicThinTrees.GraphicHalf.Stack.problemM line 59
  13. theorem OAI.AlgorithmicThinTrees.GraphicHalf.Stack.poly_problemM line 61
  14. def OAI.AlgorithmicThinTrees.GraphicHalf.Stack.problemD line 65
  15. instance OAI.AlgorithmicThinTrees.GraphicHalf.Stack.poly_problemD line 67
  16. def OAI.AlgorithmicThinTrees.GraphicHalf.Stack.extraction line 69
  17. instance OAI.AlgorithmicThinTrees.GraphicHalf.Stack.poly_extraction line 71
  18. abbrev OAI.AlgorithmicThinTrees.GraphicHalf.Stack.Problem.state line 72
  19. abbrev OAI.AlgorithmicThinTrees.GraphicHalf.Stack.Problem.active line 73
  20. abbrev OAI.AlgorithmicThinTrees.GraphicHalf.Stack.Problem.q line 74
  21. abbrev OAI.AlgorithmicThinTrees.GraphicHalf.Stack.Problem.scales line 75
  22. lemma OAI.AlgorithmicThinTrees.GraphicHalf.Stack.packingTarget_le line 77
  23. def OAI.AlgorithmicThinTrees.GraphicHalf.Stack.targetBinary line 82
  24. instance OAI.AlgorithmicThinTrees.GraphicHalf.Stack.poly_targetBinary line 84
  25. def OAI.AlgorithmicThinTrees.GraphicHalf.Stack.targetCount line 86
  26. instance OAI.AlgorithmicThinTrees.GraphicHalf.Stack.poly_targetCount line 87
  27. abbrev OAI.AlgorithmicThinTrees.GraphicHalf.Stack.Edge line 95
  28. abbrev OAI.AlgorithmicThinTrees.GraphicHalf.Stack.edgeCode line 96
  29. abbrev OAI.AlgorithmicThinTrees.GraphicHalf.Stack.context line 97
  30. abbrev OAI.AlgorithmicThinTrees.GraphicHalf.Stack.number line 98
  31. def OAI.AlgorithmicThinTrees.GraphicHalf.Stack.edgeGraphInput line 100
  32. instance OAI.AlgorithmicThinTrees.GraphicHalf.Stack.poly_edgeGraphInput line 103
  33. def OAI.AlgorithmicThinTrees.GraphicHalf.Stack.edgeActive line 105
  34. instance OAI.AlgorithmicThinTrees.GraphicHalf.Stack.poly_edgeActive line 112
  35. def OAI.AlgorithmicThinTrees.GraphicHalf.Stack.fullColumn line 114
  36. instance OAI.AlgorithmicThinTrees.GraphicHalf.Stack.poly_fullColumn line 125
  37. def OAI.AlgorithmicThinTrees.GraphicHalf.Stack.fullRows line 127
  38. instance OAI.AlgorithmicThinTrees.GraphicHalf.Stack.poly_fullRows line 129
  39. abbrev OAI.AlgorithmicThinTrees.GraphicHalf.Stack.Coordinate line 133
  40. abbrev OAI.AlgorithmicThinTrees.GraphicHalf.Stack.coordCode line 134
  41. abbrev OAI.AlgorithmicThinTrees.GraphicHalf.Stack.coordEdge line 135
  42. abbrev OAI.AlgorithmicThinTrees.GraphicHalf.Stack.coordIndex line 136
  43. lemma OAI.AlgorithmicThinTrees.GraphicHalf.Stack.graphColumns_drop line 138
  44. def OAI.AlgorithmicThinTrees.GraphicHalf.Stack.reducedEntry line 146
  45. instance OAI.AlgorithmicThinTrees.GraphicHalf.Stack.poly_reducedEntry line 153
  46. def OAI.AlgorithmicThinTrees.GraphicHalf.Stack.reducedColumn line 155
  47. instance OAI.AlgorithmicThinTrees.GraphicHalf.Stack.poly_reducedColumn line 157
  48. def OAI.AlgorithmicThinTrees.GraphicHalf.Stack.reducedRows line 159
  49. instance OAI.AlgorithmicThinTrees.GraphicHalf.Stack.poly_reducedRows line 161
  50. def OAI.AlgorithmicThinTrees.GraphicHalf.Stack.Problem.normalization line 165
  51. def OAI.AlgorithmicThinTrees.GraphicHalf.Stack.normalizationParams line 168
  52. instance OAI.AlgorithmicThinTrees.GraphicHalf.Stack.poly_normalizationParams line 171
  53. def OAI.AlgorithmicThinTrees.GraphicHalf.Stack.scales line 173
  54. instance OAI.AlgorithmicThinTrees.GraphicHalf.Stack.poly_scales line 175
  55. def OAI.AlgorithmicThinTrees.GraphicHalf.Stack.positiveMatrix line 177
  56. instance OAI.AlgorithmicThinTrees.GraphicHalf.Stack.poly_positiveMatrix line 188
  57. def OAI.AlgorithmicThinTrees.GraphicHalf.Stack.secondMatrix line 190
  58. instance OAI.AlgorithmicThinTrees.GraphicHalf.Stack.poly_secondMatrix line 194
  59. def OAI.AlgorithmicThinTrees.GraphicHalf.Stack.scaledRows line 200
  60. instance OAI.AlgorithmicThinTrees.GraphicHalf.Stack.poly_scaledRows line 208
  61. def OAI.AlgorithmicThinTrees.GraphicHalf.Stack.Problem.forms line 210
  62. def OAI.AlgorithmicThinTrees.GraphicHalf.Stack.forms line 214
  63. instance OAI.AlgorithmicThinTrees.GraphicHalf.Stack.poly_forms line 218
  64. abbrev OAI.AlgorithmicThinTrees.GraphicHalf.Stack.MaskInput line 220
  65. abbrev OAI.AlgorithmicThinTrees.GraphicHalf.Stack.maskCode line 221
  66. abbrev OAI.AlgorithmicThinTrees.GraphicHalf.Stack.maskProblem line 222
  67. abbrev OAI.AlgorithmicThinTrees.GraphicHalf.Stack.maskSigns line 223
  68. abbrev OAI.AlgorithmicThinTrees.GraphicHalf.Stack.MaskEdge line 224
  69. abbrev OAI.AlgorithmicThinTrees.GraphicHalf.Stack.maskEdgeCode line 225
  70. abbrev OAI.AlgorithmicThinTrees.GraphicHalf.Stack.maskContext line 226
  71. abbrev OAI.AlgorithmicThinTrees.GraphicHalf.Stack.maskIndex line 227
  72. def OAI.AlgorithmicThinTrees.GraphicHalf.Stack.maskEdgeInput line 229
  73. instance OAI.AlgorithmicThinTrees.GraphicHalf.Stack.poly_maskEdgeInput line 232
  74. def OAI.AlgorithmicThinTrees.GraphicHalf.Stack.maskBit line 234
  75. instance OAI.AlgorithmicThinTrees.GraphicHalf.Stack.poly_maskBit line 239
  76. def OAI.AlgorithmicThinTrees.GraphicHalf.Stack.mask line 241
  77. instance OAI.AlgorithmicThinTrees.GraphicHalf.Stack.poly_mask line 245
  78. def OAI.AlgorithmicThinTrees.GraphicHalf.Stack.signsProgram line 252
  79. def OAI.AlgorithmicThinTrees.GraphicHalf.Stack.sparsifyProgram line 254
  80. theorem OAI.AlgorithmicThinTrees.GraphicHalf.Stack.sparsify_program_polynomial line 267