OAI/Combinatorics/Progressions/Dynamics/PhysicalEpochComparison.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Erdos3.EpochSymbolRecord line 19
  2. def OAI.Erdos3.EpochSymbolRecord.Controlled line 49
  3. theorem OAI.Erdos3.EpochSymbolRecord.transport line 53
  4. def OAI.Erdos3.epochRecordIntersection line 86
  5. inductive OAI.Erdos3.EpochRecordHistory line 91
  6. theorem OAI.Erdos3.epochRecordIntersection_eq_iInf line 98
  7. theorem OAI.Erdos3.EpochRecordHistory.length_add_finrank_le line 116
  8. theorem OAI.Erdos3.EpochRecordHistory.length_le_dimension line 132
  9. theorem OAI.Erdos3.EpochRecordHistory.prepend_stack_event line 140
  10. structure OAI.Erdos3.PhysicalEpochSource line 166
  11. structure OAI.Erdos3.PhysicalEpochRecords line 194
  12. def OAI.Erdos3.PhysicalEpochRecords.empty line 204
  13. def OAI.Erdos3.PhysicalEpochRecords.dimension line 209
  14. theorem OAI.Erdos3.PhysicalEpochRecords.dimension_le line 212
  15. theorem OAI.Erdos3.exists_retained_epoch_from_records line 232
  16. theorem OAI.Erdos3.ResiduePairDimensionDrop.physical_record line 285
  17. theorem OAI.Erdos3.EpochRecordHistory.extend_of_event line 375
  18. structure OAI.Erdos3.PhysicalEpochComparison line 427
  19. theorem OAI.Erdos3.PhysicalEpochComparison.base_nonempty line 456
  20. theorem OAI.Erdos3.PhysicalEpochComparison.refined_nonempty line 460
  21. theorem OAI.Erdos3.PhysicalEpochComparison.impossible_at_zero line 464