OAI/Combinatorics/Progressions/Linear/UniformPhysicalFrameConstruction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Erdos3.PhysicalEpochFrame line 18
  2. theorem OAI.Erdos3.exists_physical_frame_precision line 60
  3. theorem OAI.Erdos3.PhysicalEpochFrame.visit line 105
  4. theorem OAI.Erdos3.exists_physical_epoch_frame line 175
  5. def OAI.Erdos3.PhysicalFrameConstructionBound line 319
  6. theorem OAI.Erdos3.PhysicalFrameConstructionBound.mono line 335
  7. theorem OAI.Erdos3.exists_uniform_physical_frame_construction line 348