OAI/Combinatorics/Progressions/Lattices/QuadraticMarkedAffine.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.QuadraticMarked.seedVector line 12
  2. theorem OAI.Erdos3.QuadraticMarked.seedVector_mem line 14
  3. def OAI.Erdos3.QuadraticMarked.affineCoefficient line 20
  4. def OAI.Erdos3.QuadraticMarked.sourceLift line 28
  5. def OAI.Erdos3.QuadraticMarked.projectedLift line 33
  6. theorem OAI.Erdos3.QuadraticMarked.sourceLift_eval line 37
  7. theorem OAI.Erdos3.QuadraticMarked.projectedLift_mem line 45
  8. theorem OAI.Erdos3.QuadraticMarked.projectedLift_pure line 50
  9. theorem OAI.Erdos3.QuadraticMarked.projectedLift_phase line 63
  10. def OAI.Erdos3.QuadraticMarked.seedCoordinate line 68
  11. theorem OAI.Erdos3.QuadraticMarked.seedCoordinate_seedVector line 72
  12. theorem OAI.Erdos3.QuadraticMarked.sourceLift_shift_coordinate line 83
  13. theorem OAI.Erdos3.QuadraticMarked.shiftedLift_coordinate line 93
  14. def OAI.Erdos3.QuadraticMarked.pureOrbit line 103
  15. theorem OAI.Erdos3.QuadraticMarked.pureOrbit_eval line 110
  16. theorem OAI.Erdos3.QuadraticMarked.pureOrbit_phase line 121
  17. theorem OAI.Erdos3.QuadraticMarked.pureOrbit_at_zero line 126