OAI/Combinatorics/UniformKServer/EpochGeometry.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Actual held vector epochs and persistent dominant identity of companion §03. The scalar cumulative-credit budget is linked by an exact projection.

  1. def OAI.UniformKServer.EpochGeometry.total line 16
  2. def OAI.UniformKServer.EpochGeometry.variation line 17
  3. def OAI.UniformKServer.EpochGeometry.side line 18
  4. structure OAI.UniformKServer.EpochGeometry.State line 22
  5. def OAI.UniformKServer.EpochGeometry.initial line 26
  6. def OAI.UniformKServer.EpochGeometry.scalar line 27
  7. def OAI.UniformKServer.EpochGeometry.valid line 28
  8. def OAI.UniformKServer.EpochGeometry.update line 32
  9. def OAI.UniformKServer.EpochGeometry.dominant line 37
  10. theorem OAI.UniformKServer.EpochGeometry.variation_nonneg line 42
  11. theorem OAI.UniformKServer.EpochGeometry.variation_self line 43
  12. theorem OAI.UniformKServer.EpochGeometry.variation_triangle line 44
  13. theorem OAI.UniformKServer.EpochGeometry.total_nonneg line 53
  14. theorem OAI.UniformKServer.EpochGeometry.total_difference line 55
  15. theorem OAI.UniformKServer.EpochGeometry.initial_valid line 59
  16. theorem OAI.UniformKServer.EpochGeometry.scalar_valid line 64
  17. theorem OAI.UniformKServer.EpochGeometry.update_valid line 68
  18. theorem OAI.UniformKServer.EpochGeometry.scalar_update line 79
  19. def OAI.UniformKServer.EpochGeometry.schedule line 85
  20. theorem OAI.UniformKServer.EpochGeometry.schedule_valid line 89
  21. theorem OAI.UniformKServer.EpochGeometry.scalar_schedule line 96
  22. theorem OAI.UniformKServer.EpochGeometry.wholesale_budget line 104
  23. theorem OAI.UniformKServer.EpochGeometry.coordinate_difference line 114
  24. theorem OAI.UniformKServer.EpochGeometry.side_difference line 119
  25. theorem OAI.UniformKServer.EpochGeometry.total_with_side line 130
  26. theorem OAI.UniformKServer.EpochGeometry.dominant_spec line 139
  27. theorem OAI.UniformKServer.EpochGeometry.absent_spec line 150
  28. theorem OAI.UniformKServer.EpochGeometry.two_le_total line 159
  29. theorem OAI.UniformKServer.EpochGeometry.regular_base line 166
  30. theorem OAI.UniformKServer.EpochGeometry.regular_size line 181
  31. theorem OAI.UniformKServer.EpochGeometry.dominant_size line 188
  32. theorem OAI.UniformKServer.EpochGeometry.total_comparison line 199