OAI/Combinatorics/Progressions/Lattices/SmoothIntegerTranslation.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.smoothAffineSample line 12
  2. theorem OAI.Erdos3.smoothAffineSample_base_injective line 16
  3. theorem OAI.Erdos3.smoothAffineSample_point_cap line 25
  4. theorem OAI.Erdos3.smoothAffineSample_energy line 34
  5. theorem OAI.Erdos3.smoothAffineSample_energy_of_sum_bound line 44
  6. theorem OAI.Erdos3.smoothAffineSample_variation line 64
  7. theorem OAI.Erdos3.smoothAffineSample_scaled_variation line 99
  8. theorem OAI.Erdos3.shiftedSmoothRowMass_pos line 122
  9. theorem OAI.Erdos3.shiftedSmoothProductPMF_rows line 128
  10. def OAI.Erdos3.smoothAffinePairRows line 139
  11. theorem OAI.Erdos3.smoothAffinePairRows_apply line 143
  12. theorem OAI.Erdos3.shiftedSmoothAffinePairRows_law line 149
  13. theorem OAI.Erdos3.smoothAffinePairRows_congruence line 173
  14. theorem OAI.Erdos3.affinePairPMF_zero_off_congruence line 180
  15. theorem OAI.Erdos3.shiftedSmoothSampleSum_integer line 198
  16. theorem OAI.Erdos3.shiftedSmoothProductMass_integer_pos line 205
  17. theorem OAI.Erdos3.shiftedSmoothCoefficientPMF_integer line 212
  18. theorem OAI.Erdos3.shiftedSmoothProductPMF_integer line 225
  19. theorem OAI.Erdos3.smoothAffinePairRows_add line 237
  20. theorem OAI.Erdos3.shiftedSmoothAffinePairRows_integer line 244
  21. theorem OAI.Erdos3.shiftedSmoothAffinePairRows_integer_apply line 255