OAI/Combinatorics/ThinTrees/Continuation/Iteration.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Continuation iteration.

  1. lemma OAI.AlgorithmicThinTrees.MetricTests.continuation_ramp_lower_of_le line 15
  2. lemma OAI.AlgorithmicThinTrees.MetricTests.stepFeasible_mono_target line 43
  3. def OAI.AlgorithmicThinTrees.MetricTests.StepFree.nextCapacity line 55
  4. lemma OAI.AlgorithmicThinTrees.MetricTests.StepFree.nextCapacity_nonneg line 58
  5. lemma OAI.AlgorithmicThinTrees.MetricTests.StepFree.nextCapacity_bounds line 61
  6. theorem OAI.AlgorithmicThinTrees.MetricTests.stepFeasible_update line 75
  7. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.search_error_le_step line 110
  8. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.target line 123
  9. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.cast_target line 125
  10. theorem OAI.AlgorithmicThinTrees.MetricTests.RationalStep.uniform_search_response line 129
  11. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.qresponse line 189
  12. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.cast_qresponse line 192
  13. structure OAI.AlgorithmicThinTrees.MetricTests.RationalStep.State line 200
  14. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.update line 206
  15. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.State.realMatrix line 213
  16. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Invariant line 216
  17. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.update_realMatrix line 223
  18. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.update_capacity line 233
  19. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.update_invariant line 245