OAI/Combinatorics/Progressions/Sampling/CoefficientGridRate.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.mem_rectangularWeightIndices_zero_of_norm_le line 12
  2. theorem OAI.Erdos3.coefficientImagePMF_zero_off_box line 26
  3. theorem OAI.Erdos3.coefficientImageMask_zero_off_box line 54
  4. def OAI.Erdos3.coefficientGridProxy line 88
  5. theorem OAI.Erdos3.coefficientGridProxy_nonneg line 93
  6. theorem OAI.Erdos3.coefficientGridProxy_integrable line 105
  7. theorem OAI.Erdos3.coefficientImage_count_error line 119
  8. theorem OAI.Erdos3.coefficientImage_polynomial_l1 line 143
  9. theorem OAI.Erdos3.normalized_selected_split_norm_le line 187
  10. def OAI.Erdos3.coefficientGridBoxFactor line 206
  11. theorem OAI.Erdos3.coefficientGridBoxFactor_pos line 209
  12. theorem OAI.Erdos3.coefficientImage_l1_of_control line 214
  13. theorem OAI.Erdos3.coefficientGridProxy_integrable_of_control line 235
  14. theorem OAI.Erdos3.coefficientImage_enormous_l1_of_control line 258