OAI/Combinatorics/Progressions/Estimates/PreparedCenteredDeterminingSlots.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.RankPreparationFamily.sortedDeterminingPolynomial line 23
  2. def OAI.Erdos3.RankPreparationFamily.sortedDeterminingMatrix line 27
  3. theorem OAI.Erdos3.RankPreparationFamily.sortedDeterminingPolynomial_support line 32
  4. theorem OAI.Erdos3.RankPreparationFamily.sortedDeterminingMatrix_weight line 42
  5. theorem OAI.Erdos3.RankPreparationFamily.sortedDeterminingPolynomial_reconstruction line 49
  6. theorem OAI.Erdos3.RankPreparationFamily.integral_determining_card line 63
  7. theorem OAI.Erdos3.RankPreparationFamily.sortedDeterminingRecovered_rank line 69
  8. def OAI.Erdos3.RankPreparationFamily.determiningPatch line 77
  9. def OAI.Erdos3.RankPreparationFamily.padDeterminingRecovered line 88
  10. theorem OAI.Erdos3.RankPreparationFamily.padDeterminingRecovered_value line 95
  11. theorem OAI.Erdos3.RankPreparationFamily.padDeterminingRecovered_lip line 102
  12. def OAI.Erdos3.RankPreparationFamily.determiningCenterCoordinate line 128
  13. theorem OAI.Erdos3.RankPreparationFamily.determiningCenterCoordinate_reconstruction line 131
  14. def OAI.Erdos3.RankPreparationFamily.sortedDeterminingCenter line 155
  15. theorem OAI.Erdos3.RankPreparationFamily.sortedDeterminingCenter_reconstruction line 159
  16. def OAI.Erdos3.RankPreparationFamily.centeredDeterminingPolynomial line 171
  17. theorem OAI.Erdos3.RankPreparationFamily.centeredDeterminingPolynomial_support line 175
  18. theorem OAI.Erdos3.RankPreparationFamily.centeredDeterminingPolynomial_reconstruction line 184
  19. theorem OAI.Erdos3.RankPreparationFamily.fullTaggedBufferedCoordinates_eq_centeredDetermining line 200
  20. def OAI.Erdos3.RankPreparationFamily.centeredDeterminingPatch line 210