OAI/Combinatorics/Progressions/Fourier/PolynomialWeightedCubeMajorArc.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.booleanBlockPhase_bounded_stride_major_arc line 17
  2. theorem OAI.Erdos3.moderateBooleanBlock_bounded_stride_major_arc line 33
  3. theorem OAI.Erdos3.weightedCubeBlock_major_arc line 63
  4. theorem OAI.Erdos3.weightedModerateBlock_major_arc line 119
  5. theorem OAI.Erdos3.affine_weightedCubeBlock_major_arc line 193
  6. theorem OAI.Erdos3.affine_weightedModerateBlock_major_arc line 244
  7. def OAI.Erdos3.NormalizedScalarCubeSource.majorArcLocalizationData line 322
  8. theorem OAI.Erdos3.NormalizedScalarCubeSource.majorArcLocalizationData_source line 327
  9. theorem OAI.Erdos3.NormalizedScalarCubeSource.majorArcLocalizationData_cellLength line 330
  10. theorem OAI.Erdos3.NormalizedScalarCubeSource.majorArcLocalizationData_error line 339
  11. theorem OAI.Erdos3.NormalizedScalarCubeSource.majorArcLocalizationData_lengthLoss line 349
  12. theorem OAI.Erdos3.polynomial_affine_weightedCubeBlock_major_arc line 369
  13. theorem OAI.Erdos3.polynomial_affine_weightedModerateBlock_major_arc line 419
  14. theorem OAI.Erdos3.polynomial_weightedCubeBlock_major_arc line 488