OAI/Combinatorics/Progressions/Linear/DeterminingMatrixDilation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.dilatedIntegerMatrix line 13
  2. theorem OAI.Erdos3.dilatedIntegerMatrix_entry_dvd line 16
  3. theorem OAI.Erdos3.dilatedIntegerMatrix_nonzero_original line 20
  4. theorem OAI.Erdos3.dilatedIntegerMatrix_nonzero_iff line 25
  5. theorem OAI.Erdos3.dilatedIntegerMatrix_support_relation line 31
  6. theorem OAI.Erdos3.dilatedIntegerMatrix_weights line 37
  7. theorem OAI.Erdos3.realIntegerMatrix_dilated_div line 43
  8. theorem OAI.Erdos3.dilatedIntegerMatrix_row_abs_sum line 54
  9. theorem OAI.Erdos3.dilatedIntegerMatrix_row_abs_sum_le line 61
  10. theorem OAI.Erdos3.dilatedIntegerMatrix_row_abs_sum_le_uniform line 67
  11. theorem OAI.Erdos3.dilatedIntegerMatrix_projection_columns line 72
  12. theorem OAI.Erdos3.recoveredIntegerLift_dilated_residue line 80
  13. theorem OAI.Erdos3.recoveredIntegerLift_dilated_projection line 86
  14. theorem OAI.Erdos3.recoveredIntegerLift_dilated_discrete_data line 92
  15. theorem OAI.Erdos3.recoveredSmallLift_dilated_div line 102