OAI/Combinatorics/Progressions/Estimates/PreparedDilatedDeterminingSlots.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.RankPreparationFamily.dilatedCenteredDeterminingPolynomial line 21
  2. def OAI.Erdos3.RankPreparationFamily.dilatedSortedDeterminingMatrix line 25
  3. theorem OAI.Erdos3.RankPreparationFamily.dilatedCenteredDeterminingPolynomial_support line 30
  4. theorem OAI.Erdos3.RankPreparationFamily.dilatedCenteredDeterminingPolynomial_eval line 38
  5. theorem OAI.Erdos3.RankPreparationFamily.dilatedCenteredDeterminingPolynomial_reconstruction line 45
  6. theorem OAI.Erdos3.RankPreparationFamily.fullTaggedBufferedCoordinates_eq_dilatedCenteredDetermining line 54
  7. theorem OAI.Erdos3.RankPreparationFamily.dilatedSortedDeterminingMatrix_dvd line 64
  8. theorem OAI.Erdos3.RankPreparationFamily.dilatedSortedDeterminingMatrix_weight line 70
  9. theorem OAI.Erdos3.RankPreparationFamily.dilatedSortedDeterminingMatrix_row_abs_sum_le line 80
  10. theorem OAI.Erdos3.RankPreparationFamily.dilatedSortedDeterminingMatrix_row_abs_sum_le_exp line 86
  11. def OAI.Erdos3.RankPreparationFamily.dilatedCenteredDeterminingPatch line 96
  12. theorem OAI.Erdos3.RankPreparationFamily.dilatedCenteredDeterminingPatch_weight line 107
  13. theorem OAI.Erdos3.RankPreparationFamily.dilatedCenteredDeterminingPatch_kernel line 113