OAI/Combinatorics/ThinTrees/Normalization/Realization.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

Normalization realization.

  1. def OAI.CurrentKS.Realization.selectFlagged line 22
  2. instance OAI.CurrentKS.Realization.poly_selectFlagged line 32
  3. lemma OAI.CurrentKS.Realization.find_map_flagged line 36
  4. structure OAI.AlgorithmicThinTrees.Normalization.Stack.Params line 52
  5. abbrev OAI.AlgorithmicThinTrees.Normalization.Stack.paramsDataCode line 59
  6. def OAI.AlgorithmicThinTrees.Normalization.Stack.Params.data line 61
  7. def OAI.AlgorithmicThinTrees.Normalization.Stack.paramsCode line 62
  8. abbrev OAI.AlgorithmicThinTrees.Normalization.Stack.view line 63
  9. instance OAI.AlgorithmicThinTrees.Normalization.Stack.poly_view line 65
  10. abbrev OAI.AlgorithmicThinTrees.Normalization.Stack.dim line 69
  11. abbrev OAI.AlgorithmicThinTrees.Normalization.Stack.rest line 70
  12. abbrev OAI.AlgorithmicThinTrees.Normalization.Stack.count line 71
  13. abbrev OAI.AlgorithmicThinTrees.Normalization.Stack.tail line 72
  14. abbrev OAI.AlgorithmicThinTrees.Normalization.Stack.factor line 73
  15. abbrev OAI.AlgorithmicThinTrees.Normalization.Stack.columns line 74
  16. def OAI.AlgorithmicThinTrees.Normalization.Stack.numColumns line 75
  17. instance OAI.AlgorithmicThinTrees.Normalization.Stack.poly_numColumns line 79
  18. def OAI.AlgorithmicThinTrees.Normalization.Stack.outer line 83
  19. instance OAI.AlgorithmicThinTrees.Normalization.Stack.poly_outer line 87
  20. lemma OAI.AlgorithmicThinTrees.Normalization.Stack.outer_data line 90
  21. structure OAI.AlgorithmicThinTrees.Normalization.Stack.State line 96
  22. def OAI.AlgorithmicThinTrees.Normalization.Stack.stateCode line 100
  23. abbrev OAI.AlgorithmicThinTrees.Normalization.Stack.stateView line 102
  24. instance OAI.AlgorithmicThinTrees.Normalization.Stack.poly_stateView line 106
  25. abbrev OAI.AlgorithmicThinTrees.Normalization.Stack.params line 110
  26. abbrev OAI.AlgorithmicThinTrees.Normalization.Stack.scales line 111
  27. def OAI.AlgorithmicThinTrees.Normalization.Stack.gram line 113
  28. instance OAI.AlgorithmicThinTrees.Normalization.Stack.poly_gram line 126
  29. abbrev OAI.AlgorithmicThinTrees.Normalization.Stack.Column line 130
  30. abbrev OAI.AlgorithmicThinTrees.Normalization.Stack.columnCode line 131
  31. abbrev OAI.AlgorithmicThinTrees.Normalization.Stack.colState line 132
  32. abbrev OAI.AlgorithmicThinTrees.Normalization.Stack.colIndex line 133
  33. abbrev OAI.AlgorithmicThinTrees.Normalization.Stack.colParams line 134
  34. def OAI.AlgorithmicThinTrees.Normalization.Stack.column line 136
  35. def OAI.AlgorithmicThinTrees.Normalization.Stack.scale line 140
  36. instance OAI.AlgorithmicThinTrees.Normalization.Stack.poly_column line 144
  37. instance OAI.AlgorithmicThinTrees.Normalization.Stack.poly_scale line 145
  38. def OAI.AlgorithmicThinTrees.Normalization.Stack.thresholdProgram line 147
  39. instance OAI.AlgorithmicThinTrees.Normalization.Stack.poly_thresholdProgram line 151
  40. def OAI.AlgorithmicThinTrees.Normalization.Stack.testProgram line 164
  41. instance OAI.AlgorithmicThinTrees.Normalization.Stack.poly_testProgram line 181
  42. def OAI.AlgorithmicThinTrees.Normalization.Stack.isHeavy line 185
  43. instance OAI.AlgorithmicThinTrees.Normalization.Stack.poly_isHeavy line 193
  44. def OAI.AlgorithmicThinTrees.Normalization.Stack.updated line 195
  45. instance OAI.AlgorithmicThinTrees.Normalization.Stack.poly_updated line 199
  46. def OAI.AlgorithmicThinTrees.Normalization.Stack.newScales line 201
  47. instance OAI.AlgorithmicThinTrees.Normalization.Stack.poly_newScales line 215
  48. def OAI.AlgorithmicThinTrees.Normalization.Stack.State.next line 217
  49. def OAI.AlgorithmicThinTrees.Normalization.Stack.step line 219
  50. instance OAI.AlgorithmicThinTrees.Normalization.Stack.poly_step line 221
  51. lemma OAI.AlgorithmicThinTrees.Normalization.Stack.next_iterate line 223
  52. lemma OAI.AlgorithmicThinTrees.Normalization.Stack.advance_iterate_parts line 232
  53. instance OAI.AlgorithmicThinTrees.Normalization.Stack.size_step line 252
  54. def OAI.AlgorithmicThinTrees.Normalization.Stack.initial line 288
  55. instance OAI.AlgorithmicThinTrees.Normalization.Stack.poly_initial line 296
  56. def OAI.AlgorithmicThinTrees.Normalization.Stack.run line 298
  57. instance OAI.AlgorithmicThinTrees.Normalization.Stack.poly_run line 305
  58. def OAI.AlgorithmicThinTrees.Normalization.Stack.unaryPow line 307
  59. instance OAI.AlgorithmicThinTrees.Normalization.Stack.poly_unaryPow line 312
  60. abbrev OAI.AlgorithmicThinTrees.Normalization.Stack.fixedCode line 317
  61. abbrev OAI.AlgorithmicThinTrees.Normalization.Stack.fixedParams line 318
  62. abbrev OAI.AlgorithmicThinTrees.Normalization.Stack.fixedR line 319
  63. def OAI.AlgorithmicThinTrees.Normalization.Stack.multiplierProgram line 321
  64. instance OAI.AlgorithmicThinTrees.Normalization.Stack.poly_multiplierProgram line 324
  65. def OAI.AlgorithmicThinTrees.Normalization.Stack.fixedStepParams line 327
  66. def OAI.AlgorithmicThinTrees.Normalization.Stack.fixedStep line 329
  67. instance OAI.AlgorithmicThinTrees.Normalization.Stack.poly_fixedStep line 333
  68. def OAI.AlgorithmicThinTrees.Normalization.Stack.lengthProgram line 335
  69. instance OAI.AlgorithmicThinTrees.Normalization.Stack.poly_lengthProgram line 341
  70. def OAI.AlgorithmicThinTrees.Normalization.Stack.normalized line 343
  71. instance OAI.AlgorithmicThinTrees.Normalization.Stack.poly_normalized line 346