OAI/Combinatorics/Progressions/Fourier/CanonicalDensityFourier.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_ambient_torus_fourier_approximation line 15
  2. theorem OAI.Erdos3.exists_crtProgressionWeight_fourier line 73
  3. theorem OAI.Erdos3.subspaceAmbientTorus_character line 120
  4. theorem OAI.Erdos3.exists_subspace_ambient_fourier_approximation line 133
  5. theorem OAI.Erdos3.exists_local_subspace_fourier_density line 163
  6. def OAI.Erdos3.smallBoxTorusKernel line 228
  7. theorem OAI.Erdos3.smallBoxTorusKernel_local line 232
  8. theorem OAI.Erdos3.smallBoxTorusKernel_lipschitz line 239
  9. theorem OAI.Erdos3.smallBoxTorusKernel_range line 247
  10. theorem OAI.Erdos3.exists_small_box_fourier_approximation line 253
  11. theorem OAI.Erdos3.smallBoxTorusKernel_nonzero_quarter_lift line 294
  12. theorem OAI.Erdos3.smallBoxTorusKernel_zero_outside_quarter line 321
  13. theorem OAI.Erdos3.coordinate_integer_translate_sub_mem line 344
  14. theorem OAI.Erdos3.exists_coordinate_integer_translate line 354
  15. def OAI.Erdos3.canonicalAmbientTorusDensity line 367
  16. theorem OAI.Erdos3.canonicalAmbientTorusDensity_eq line 371
  17. theorem OAI.Erdos3.canonicalAmbientTorusDensity_bounds line 413
  18. theorem OAI.Erdos3.canonicalAmbientTorusDensity_eq_of_support_bounds line 444
  19. theorem OAI.Erdos3.exists_canonical_density_fourier_approximation line 458