OAI/Analysis/Steinitz/Energy.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Telescoping matrix energy and trace budgets.

  1. def OAI.EuclideanSteinitz.Energy.pTrace line 12
  2. def OAI.EuclideanSteinitz.Energy.hTrace line 13
  3. lemma OAI.EuclideanSteinitz.Energy.pTrace_mono line 15
  4. lemma OAI.EuclideanSteinitz.Energy.gainValue_mono line 21
  5. lemma OAI.EuclideanSteinitz.Energy.trace_contraction line 27
  6. lemma OAI.EuclideanSteinitz.Energy.pTrace_contraction line 53
  7. lemma OAI.EuclideanSteinitz.Energy.gainValue_contraction line 57
  8. def OAI.EuclideanSteinitz.Energy.stepCost line 61
  9. def OAI.EuclideanSteinitz.Energy.cost line 64
  10. def OAI.EuclideanSteinitz.Energy.finish line 68
  11. lemma OAI.EuclideanSteinitz.Energy.Move.old_le_next line 72
  12. lemma OAI.EuclideanSteinitz.Energy.step_bounds line 76
  13. lemma OAI.EuclideanSteinitz.Energy.stepCost_nonneg line 87
  14. lemma OAI.EuclideanSteinitz.Energy.cost_nonneg line 93
  15. lemma OAI.EuclideanSteinitz.Energy.gainCost_le_cost line 102
  16. lemma OAI.EuclideanSteinitz.Energy.trace_change_le_cost line 113
  17. lemma OAI.EuclideanSteinitz.Energy.finish_eq_follow line 125
  18. lemma OAI.EuclideanSteinitz.Energy.finish_eq_follow_zero line 135
  19. lemma OAI.EuclideanSteinitz.Energy.endpoint_cost line 139
  20. lemma OAI.EuclideanSteinitz.Energy.gainConstant_one_le line 162
  21. lemma OAI.EuclideanSteinitz.Energy.sizeTrace_nonneg line 169
  22. def OAI.EuclideanSteinitz.Energy.incrementConstant line 178
  23. lemma OAI.EuclideanSteinitz.Energy.incrementConstant_pos line 181
  24. lemma OAI.EuclideanSteinitz.Energy.cost_power_bound line 186
  25. lemma OAI.EuclideanSteinitz.Energy.endpoint_cost_power line 200
  26. lemma OAI.EuclideanSteinitz.Coefficient.weighted_increment line 223