OAI/Combinatorics/Progressions/Linear/MarkedProjectionBounds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_markedShift_bounded_basis line 21
  2. theorem OAI.Erdos3.exists_markedShiftLayer_coordinate_basis line 42
  3. theorem OAI.Erdos3.exists_markedShiftQuotient_bounded_coordinates line 87
  4. theorem OAI.Erdos3.exists_markedShiftQuotientLayer_bounded_basis line 123
  5. theorem OAI.Erdos3.markedShiftPhase_coordinate_height line 174
  6. theorem OAI.Erdos3.markedShiftEval_zero_coordinate_height line 181
  7. theorem OAI.Erdos3.markedQuotientPhase_coordinate_height line 199
  8. theorem OAI.Erdos3.markedBaseEvaluation_zero_coordinate_height line 218