OAI/Combinatorics/Progressions/Dynamics/ScheduledPhysicalEpochStack.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.physicalEpochBudget line 9
  2. theorem OAI.Erdos3.physicalEpochBudget_nonneg line 13
  3. theorem OAI.Erdos3.physicalEpochBudget_work_le line 19
  4. theorem OAI.Erdos3.physicalEpochBudget_mono line 29
  5. theorem OAI.Erdos3.exists_physicalEpochBudget_power line 40
  6. inductive OAI.Erdos3.PhysicalEpochStack line 75
  7. def OAI.Erdos3.PhysicalEpochStack.dimensions line 86
  8. theorem OAI.Erdos3.PhysicalEpochStack.dimensions_length line 91
  9. theorem OAI.Erdos3.PhysicalEpochStack.dimensions_bounded line 96
  10. inductive OAI.Erdos3.PhysicalEpochStack.Event line 106
  11. theorem OAI.Erdos3.PhysicalEpochStack.Event.to_dimension_event line 121
  12. theorem OAI.Erdos3.PhysicalEpochStack.Event.rank_lt line 140
  13. theorem OAI.Erdos3.PhysicalEpochStack.event_chain_bound line 145
  14. def OAI.Erdos3.PhysicalEpochStack.RootState line 167
  15. def OAI.Erdos3.PhysicalEpochStack.UniformAt line 171
  16. theorem OAI.Erdos3.PhysicalEpochStack.UniformAt.mono line 181
  17. def OAI.Erdos3.PhysicalEpochStack.AlignedAt line 206
  18. def OAI.Erdos3.PhysicalEpochStack.BudgetedAt line 213
  19. theorem OAI.Erdos3.PhysicalEpochStack.UniformAt.aligned line 221
  20. theorem OAI.Erdos3.PhysicalEpochStack.UniformAt.budgeted line 230
  21. theorem OAI.Erdos3.PhysicalEpochStack.AlignedAt.refine line 239
  22. theorem OAI.Erdos3.PhysicalEpochStack.BudgetedAt.mono line 251
  23. def OAI.Erdos3.PhysicalEpochStack.RootCreatedAt line 274
  24. def OAI.Erdos3.PhysicalEpochStack.ScheduledAt line 278
  25. theorem OAI.Erdos3.PhysicalEpochStack.ScheduledAt.record_le line 290
  26. theorem OAI.Erdos3.PhysicalEpochStack.ScheduledAt.inflation line 294
  27. theorem OAI.Erdos3.PhysicalEpochStack.ScheduledAt.budgeted line 300