OAI/Combinatorics/ThinTrees/Continuation/Gains.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Continuation gains.

  1. def OAI.AlgorithmicThinTrees.MetricTests.booleanResponse line 18
  2. lemma OAI.AlgorithmicThinTrees.MetricTests.booleanResponse_bounds line 21
  3. lemma OAI.AlgorithmicThinTrees.MetricTests.good_capacity_nondecreasing line 26
  4. lemma OAI.AlgorithmicThinTrees.MetricTests.good_capacity_unsaturated line 35
  5. lemma OAI.AlgorithmicThinTrees.MetricTests.bad_capacity_loss line 40
  6. lemma OAI.AlgorithmicThinTrees.MetricTests.inactive_capacity line 45
  7. lemma OAI.AlgorithmicThinTrees.MetricTests.capacity_change_active line 50
  8. lemma OAI.AlgorithmicThinTrees.MetricTests.capacity_change_loss line 63
  9. lemma OAI.AlgorithmicThinTrees.MetricTests.capacity_change_gain line 84
  10. lemma OAI.AlgorithmicThinTrees.MetricTests.large_count_bound line 111
  11. lemma OAI.AlgorithmicThinTrees.MetricTests.active_capacity_sum_le line 119
  12. lemma OAI.AlgorithmicThinTrees.MetricTests.many_edges_half_unsaturated line 126
  13. lemma OAI.AlgorithmicThinTrees.MetricTests.few_edges_loss_bound line 138
  14. lemma OAI.AlgorithmicThinTrees.MetricTests.many_edges_gain_bound line 153