OAI/Combinatorics/Progressions/Fourier/SectionRetainedFourier.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.BooleanCubeKernel.affineCubeFourierSum line 16
  2. def OAI.Erdos3.BooleanCubeKernel.affineCubeFourierProjection line 23
  3. theorem OAI.Erdos3.BooleanCubeKernel.exists_affine_cube_fourier_projection line 43
  4. theorem OAI.Erdos3.BooleanCubeKernel.exists_anchored_affine_cube_fourier_projection line 129
  5. def OAI.Erdos3.BooleanCubeKernel.retainedSiteFourierSum line 216
  6. theorem OAI.Erdos3.BooleanCubeKernel.retainedSiteFourierSum_norm_le line 225
  7. theorem OAI.Erdos3.BooleanCubeKernel.exists_geometric_site_fourier_projection line 240
  8. theorem OAI.Erdos3.BooleanCubeKernel.exists_fixed_kernel_site_fourier_projection line 298
  9. def OAI.Erdos3.BooleanCubeKernel.sectionSiteFrequency line 360
  10. theorem OAI.Erdos3.BooleanCubeKernel.sectionSiteFrequency_bound line 366
  11. theorem OAI.Erdos3.BooleanCubeKernel.section_retained_fourier_sum line 376