OAI/Combinatorics/Progressions/Linear/PreparedDeterminingMatrixBudget.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.RankPreparationFamily.determiningMatrix_row_abs_sum line 19
  2. theorem OAI.Erdos3.RankPreparationFamily.sortedDeterminingMatrix_row_abs_sum line 37
  3. theorem OAI.Erdos3.RankPreparationFamily.sortedDeterminingMatrix_row_abs_sum_le line 45
  4. theorem OAI.Erdos3.RankPreparationFamily.sortedDeterminingMatrix_row_abs_sum_le_of_basis_norm line 57
  5. theorem OAI.Erdos3.RankPreparationLayer.rank_le_coord_card line 84
  6. theorem OAI.Erdos3.RankPreparationLayer.shortIntegralBasisNormBound_le_exp line 90
  7. theorem OAI.Erdos3.RankPreparationLayer.exists_bounded_integral_basis line 160
  8. def OAI.Erdos3.preparedIntegralBasisExponent line 175
  9. theorem OAI.Erdos3.RankPreparationFamily.PreparedHeights.exists_bounded_integral_bases line 182
  10. theorem OAI.Erdos3.RankPreparationFamily.PreparedHeights.exists_bounded_integral_bases_of_sized line 207
  11. theorem OAI.Erdos3.RankPreparationFamily.sortedDeterminingMatrix_row_abs_sum_le_exp line 243