OAI/Combinatorics/ThinTrees/Continuation/Encoding.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Continuation encoding.

  1. def OAI.AlgorithmicThinTrees.MetricTests.responseMatrix line 18
  2. lemma OAI.AlgorithmicThinTrees.MetricTests.responseMatrix_hermitian line 21
  3. lemma OAI.AlgorithmicThinTrees.MetricTests.responseMatrix_ones line 28
  4. lemma OAI.AlgorithmicThinTrees.MetricTests.responseMatrix_fixed line 31
  5. lemma OAI.AlgorithmicThinTrees.MetricTests.responseMatrix_add line 36
  6. lemma OAI.AlgorithmicThinTrees.MetricTests.responseMatrix_smul line 41
  7. lemma OAI.AlgorithmicThinTrees.MetricTests.responseMatrix_sub line 46
  8. abbrev OAI.AlgorithmicThinTrees.MetricTests.StepFree line 51
  9. def OAI.AlgorithmicThinTrees.MetricTests.StepFree.matrix line 56
  10. def OAI.AlgorithmicThinTrees.MetricTests.StepFree.multiplier line 57
  11. def OAI.AlgorithmicThinTrees.MetricTests.StepFree.y line 58
  12. def OAI.AlgorithmicThinTrees.MetricTests.StepFree.z line 59
  13. def OAI.AlgorithmicThinTrees.MetricTests.StepFree.capacities line 61
  14. def OAI.AlgorithmicThinTrees.MetricTests.StepFree.lowerPencil line 64
  15. def OAI.AlgorithmicThinTrees.MetricTests.StepFree.upperPencil line 65
  16. def OAI.AlgorithmicThinTrees.MetricTests.StepFree.edgePencil line 68
  17. lemma OAI.AlgorithmicThinTrees.MetricTests.StepFree.matrix_combo line 71
  18. lemma OAI.AlgorithmicThinTrees.MetricTests.StepFree.lowerPencil_combo line 77
  19. lemma OAI.AlgorithmicThinTrees.MetricTests.StepFree.upperPencil_combo line 85
  20. lemma OAI.AlgorithmicThinTrees.MetricTests.StepFree.edgePencil_combo line 97
  21. lemma OAI.AlgorithmicThinTrees.MetricTests.StepFree.capacities_combo line 103
  22. def OAI.AlgorithmicThinTrees.MetricTests.stepCore line 113
  23. def OAI.AlgorithmicThinTrees.MetricTests.stepFeasible line 120
  24. lemma OAI.AlgorithmicThinTrees.MetricTests.stepCore_domain line 123
  25. lemma OAI.AlgorithmicThinTrees.MetricTests.stepCore_admissible line 129
  26. lemma OAI.AlgorithmicThinTrees.MetricTests.stepCore_capacity_le line 134
  27. lemma OAI.AlgorithmicThinTrees.MetricTests.stepFeasible_response line 143
  28. lemma OAI.AlgorithmicThinTrees.MetricTests.response_to_stepFeasible line 153