OAI/Combinatorics/Progressions/Lattices/CRTProgressionVanishing.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.progression_window_radius_bounds line 11
  2. theorem OAI.Erdos3.residue_base_window_bound line 16
  3. theorem OAI.Erdos3.residue_step_window_bounds line 29
  4. theorem OAI.Erdos3.residue_progression_val_of_windows line 56
  5. def OAI.Erdos3.progressionTorusCenter line 75
  6. def OAI.Erdos3.progressionTorusCutoff line 78
  7. theorem OAI.Erdos3.progressionTorusCutoff_range line 82
  8. theorem OAI.Erdos3.progressionTorusCutoff_lipschitz line 87
  9. theorem OAI.Erdos3.progressionTorusCutoff_residue_support line 91
  10. theorem OAI.Erdos3.progressionTorusCutoff_residue_mean line 108
  11. def OAI.Erdos3.crtProgressionWeight line 118
  12. theorem OAI.Erdos3.crtProgressionWeight_range line 123
  13. theorem OAI.Erdos3.crtProgressionWeight_mean line 129
  14. theorem OAI.Erdos3.crtProgressionWeight_support line 141
  15. def OAI.Erdos3.IntegerVectorAPFree line 168
  16. def OAI.Erdos3.residueBoxIntegerPoint line 171
  17. theorem OAI.Erdos3.crtProgressionWeight_mul_prod_eq_zero line 174
  18. theorem OAI.Erdos3.crtProgressionWeight_product_mean_eq_zero line 206