OAI/Combinatorics/Progressions/Lattices/AffineCubePositiveComparison.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.BooleanCubeKernel.exists_affine_cube_approximated_projection line 13
  2. theorem OAI.Erdos3.BooleanCubeKernel.affineCubeModeFactors_iff_bounded line 80
  3. theorem OAI.Erdos3.BooleanCubeKernel.exists_affine_cube_residual line 105
  4. theorem OAI.Erdos3.BooleanCubeKernel.coefficientResidual_section_integrable line 145
  5. theorem OAI.Erdos3.BooleanCubeKernel.coefficientResidualAverage_continuous line 156
  6. theorem OAI.Erdos3.BooleanCubeKernel.coefficientTorusFourierSum_residualAverage line 167
  7. theorem OAI.Erdos3.BooleanCubeKernel.affineCubeFourierProjection_eq_residualAverage line 191
  8. theorem OAI.Erdos3.BooleanCubeKernel.coefficientTorusFourierProjection_approx_residualAverage line 206
  9. theorem OAI.Erdos3.BooleanCubeKernel.exists_affine_cube_positive_density line 243
  10. theorem OAI.Erdos3.BooleanCubeKernel.exists_affine_cube_positive_comparison line 288