OAI/Combinatorics/Progressions/Estimates/ShiftedProductTestError.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.shiftedSmoothSamples_count_integral line 14
  2. theorem OAI.Erdos3.shiftedSmoothSamples_center_l1 line 23
  3. theorem OAI.Erdos3.shiftedSmoothCoefficientPMF_center_l1 line 53
  4. theorem OAI.Erdos3.pmf_image_complex_sum_eq_count_integral line 96
  5. theorem OAI.Erdos3.pmf_image_count_test_error line 115
  6. theorem OAI.Erdos3.pmf_projected_count_test_error line 125
  7. theorem OAI.Erdos3.shiftedSmoothProductMass_pos_of_large line 151
  8. theorem OAI.Erdos3.shiftedSmoothProductPMF_zero line 157
  9. theorem OAI.Erdos3.shiftedSmoothProductPMF_center_l1 line 169
  10. theorem OAI.Erdos3.shiftedSmoothProductPMF_center_test line 196
  11. theorem OAI.Erdos3.shiftedSmoothProductPMF_recenter_test line 212
  12. theorem OAI.Erdos3.BooleanCubeKernel.selectedResidue_covered_reconstruction_comparison line 234
  13. theorem OAI.Erdos3.shiftedSmoothProductPMF_matrix_image line 309
  14. theorem OAI.Erdos3.shiftedProductImage_count_error line 324
  15. def OAI.Erdos3.shiftedProductGridProxy line 379
  16. theorem OAI.Erdos3.shiftedProductGridProxy_integrable line 386
  17. theorem OAI.Erdos3.shiftedProduct_test_error line 398