OAI/Combinatorics/Progressions/Estimates/PhysicalStabilityParameters.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.PhysicalEpochStack.periods line 18
  2. theorem OAI.Erdos3.PhysicalEpochStack.periods_length line 22
  3. theorem OAI.Erdos3.PhysicalEpochStack.periods_product_pos line 27
  4. theorem OAI.Erdos3.PhysicalEpochStack.period_dvd_product line 32
  5. theorem OAI.Erdos3.PhysicalEpochStack.UniformAt.periods_product_le line 35
  6. theorem OAI.Erdos3.PhysicalEpochStack.UniformAt.period_exclusions_card_le line 55
  7. theorem OAI.Erdos3.PhysicalEpochStack.pending_coprime_periods line 65
  8. inductive OAI.Erdos3.PhysicalEpochStack.RecordEvent line 90
  9. theorem OAI.Erdos3.exists_physical_stack_record_descent line 106
  10. theorem OAI.Erdos3.exists_scheduled_physical_epoch_stack line 167
  11. theorem OAI.Erdos3.PhysicalEpochStack.RecordEvent.rebuild line 235
  12. theorem OAI.Erdos3.exists_scheduled_physical_event_parameters line 300
  13. structure OAI.Erdos3.PhysicalStabilityParameters line 356
  14. theorem OAI.Erdos3.exists_physical_stability_parameters line 384