OAI/Combinatorics/ThinTrees/Sparsification/RationalIteration.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Rational iteration.

  1. def OAI.AlgorithmicThinTrees.Iteration.iterate line 18
  2. def OAI.AlgorithmicThinTrees.Iteration.RoundBound line 28
  3. lemma OAI.AlgorithmicThinTrees.Iteration.iterate_bound line 36
  4. def OAI.AlgorithmicThinTrees.Iteration.initialCount line 84
  5. lemma OAI.AlgorithmicThinTrees.Iteration.initialCount_pos line 85
  6. lemma OAI.AlgorithmicThinTrees.Iteration.initialCount_lower line 86
  7. lemma OAI.AlgorithmicThinTrees.Iteration.initial_packable line 90
  8. def OAI.AlgorithmicThinTrees.Iteration.tree line 109
  9. theorem OAI.AlgorithmicThinTrees.Iteration.tree_correct line 112