OAI/Combinatorics/ThinTrees/Continuation/Grid.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Continuation grid.

  1. def OAI.AlgorithmicThinTrees.MetricTests.StepFree.canonical line 18
  2. lemma OAI.AlgorithmicThinTrees.MetricTests.StepFree.canonical_matrix line 20
  3. lemma OAI.AlgorithmicThinTrees.MetricTests.StepFree.canonical_core line 24
  4. lemma OAI.AlgorithmicThinTrees.MetricTests.StepFree.canonical_feasible line 32
  5. def OAI.AlgorithmicThinTrees.MetricTests.StepFree.Bounded line 37
  6. lemma OAI.AlgorithmicThinTrees.MetricTests.StepFree.Bounded.combo line 41
  7. lemma OAI.AlgorithmicThinTrees.MetricTests.StepFree.canonical_bound line 55
  8. lemma OAI.AlgorithmicThinTrees.MetricTests.auxiliaryPoint_canonical line 88
  9. lemma OAI.AlgorithmicThinTrees.MetricTests.baseline_le_one line 94
  10. theorem OAI.AlgorithmicThinTrees.MetricTests.bounded_step_inner_cube line 98
  11. abbrev OAI.AlgorithmicThinTrees.MetricTests.StepIntegers line 125
  12. abbrev OAI.AlgorithmicThinTrees.MetricTests.StepRational line 128
  13. def OAI.AlgorithmicThinTrees.MetricTests.StepRational.real line 133
  14. def OAI.AlgorithmicThinTrees.MetricTests.StepIntegers.onGrid line 141
  15. def OAI.AlgorithmicThinTrees.MetricTests.StepIntegers.Bounded line 145
  16. def OAI.AlgorithmicThinTrees.MetricTests.roundStep line 151
  17. lemma OAI.AlgorithmicThinTrees.MetricTests.floorGrid_error line 155
  18. lemma OAI.AlgorithmicThinTrees.MetricTests.roundStep_error line 166
  19. lemma OAI.AlgorithmicThinTrees.MetricTests.floorGrid_bound line 182
  20. lemma OAI.AlgorithmicThinTrees.MetricTests.roundStep_bound line 200
  21. theorem OAI.AlgorithmicThinTrees.MetricTests.bounded_grid_step line 209
  22. theorem OAI.AlgorithmicThinTrees.MetricTests.uniform_continuation_grid line 228