OAI/Combinatorics/ThinTrees/Sparsification/ShortcutExtraction.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Shortcut extraction.

  1. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.State.active line 16
  2. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.State.packingTarget line 18
  3. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.active_mem line 20
  4. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.baseline_total_lt_one line 24
  5. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.sum_capacity_le_active line 29
  6. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.active_packable line 55
  7. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.packingTarget_lower line 78
  8. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.packingTarget_upper line 85
  9. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.packingTarget_pos line 90
  10. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.active_resistance line 94
  11. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.rounding_absorbed line 109
  12. theorem OAI.AlgorithmicThinTrees.MetricTests.RationalStep.shortcut_correct line 118