OAI/Combinatorics/ThinTrees/Continuation/Schedule.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Continuation schedule.

  1. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.nthRoot_le_real_root line 15
  2. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.real_root_lt_nthRoot_add line 21
  3. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.nthRoot_pos line 27
  4. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.gain line 32
  5. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.blocks line 34
  6. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.blockLength line 36
  7. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.scheduleLength line 38
  8. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.gain_bounds line 40
  9. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.blockLength_step line 62
  10. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.blocks_le_root line 67
  11. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.schedule_loss_bound line 70
  12. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.large_blocks line 83
  13. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.large_gain line 86
  14. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.large_schedule_loss line 101
  15. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.block_growth line 111
  16. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.fourth_power_le_two_pow line 118
  17. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.schedule_growth line 134
  18. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.schedule_length_bound line 148
  19. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.scheduleLength_step line 155
  20. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.cost_le_schedule line 161
  21. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.running_quality_lower line 170
  22. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.running_quality_loss line 176