OAI/Combinatorics/ThinTrees/Continuation/Search.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Continuation search.

  1. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.sizeQ line 15
  2. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.baselineQ line 16
  3. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.stepQ line 17
  4. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.radiusQ line 18
  5. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.boundQ line 19
  6. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.errorQ line 20
  7. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.cast_sizeQ line 22
  8. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.cast_baselineQ line 24
  9. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.cast_stepQ line 26
  10. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.cast_radiusQ line 28
  11. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.cast_boundQ line 30
  12. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.cast_errorQ line 32
  13. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.sizeQ_two line 35
  14. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.radiusQ_pos line 38
  15. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.radiusQ_le_one line 40
  16. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.boundQ_nonneg line 43
  17. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.search line 47
  18. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.coordinate_ball line 51
  19. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.center_norm line 62
  20. theorem OAI.AlgorithmicThinTrees.MetricTests.RationalStep.search_sound line 77
  21. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.search_fuel_bound line 109
  22. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.search_on_mesh line 141