OAI/Combinatorics/ThinTrees/Continuation/Margin.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Continuation margin.

  1. lemma OAI.AlgorithmicThinTrees.Partitions.partCount_le_card line 15
  2. lemma OAI.AlgorithmicThinTrees.Partitions.crossingIndicator_le_one line 19
  3. lemma OAI.AlgorithmicThinTrees.Partitions.slack_combo line 24
  4. lemma OAI.AlgorithmicThinTrees.Partitions.slack_change_target line 33
  5. lemma OAI.AlgorithmicThinTrees.MetricTests.StepFree.multiplier_combo line 51
  6. lemma OAI.AlgorithmicThinTrees.MetricTests.StepFree.y_combo line 54
  7. lemma OAI.AlgorithmicThinTrees.MetricTests.StepFree.z_combo line 57
  8. lemma OAI.AlgorithmicThinTrees.MetricTests.StepFree.Close.refl line 60
  9. lemma OAI.AlgorithmicThinTrees.MetricTests.StepFree.close_add_rescale line 64
  10. lemma OAI.AlgorithmicThinTrees.MetricTests.StepFree.Close.capacities line 77
  11. lemma OAI.AlgorithmicThinTrees.MetricTests.StepFree.Close.slack line 85
  12. lemma OAI.AlgorithmicThinTrees.MetricTests.stepCore_convex line 103
  13. lemma OAI.AlgorithmicThinTrees.MetricTests.stepFeasible_convex line 139
  14. lemma OAI.AlgorithmicThinTrees.MetricTests.convex_innerCube line 146
  15. lemma OAI.AlgorithmicThinTrees.MetricTests.auxiliary_slack line 157
  16. lemma OAI.AlgorithmicThinTrees.MetricTests.mixing_numbers line 189
  17. theorem OAI.AlgorithmicThinTrees.MetricTests.step_inner_cube line 226
  18. lemma OAI.AlgorithmicThinTrees.MetricTests.gain_at_least_one line 277
  19. lemma OAI.AlgorithmicThinTrees.MetricTests.continuation_margin_lower line 287
  20. theorem OAI.AlgorithmicThinTrees.MetricTests.uniform_continuation_inner_cube line 298