OAI/Combinatorics/Progressions/Estimates/SubspaceLayeredModeSmoothRemoval.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.smoothProductPMF_translation_test_le line 13
  2. theorem OAI.Erdos3.smoothProductPMF_toReal_sum line 46
  3. theorem OAI.Erdos3.smoothProductPMF_toReal_zero_off line 52
  4. theorem OAI.Erdos3.smoothProductPMF_shift_transfer line 60
  5. theorem OAI.Erdos3.smooth_row_shift_transfer line 96
  6. theorem OAI.Erdos3.VectorPolynomial.coefficient_mode_finite_removal line 132
  7. def OAI.Erdos3.VectorPolynomial.coefficientModeTestedPhase line 179
  8. theorem OAI.Erdos3.VectorPolynomial.coefficientModeTestedPhase_norm_le line 188
  9. theorem OAI.Erdos3.VectorPolynomial.coefficient_mode_smooth_removal line 197
  10. def OAI.Erdos3.VectorPolynomial.lowerModePolynomial line 249
  11. theorem OAI.Erdos3.VectorPolynomial.lowerModePolynomial_degree line 254
  12. theorem OAI.Erdos3.VectorPolynomial.lowerModePolynomial_eval line 265
  13. theorem OAI.Erdos3.VectorPolynomial.coefficientModeTestedPhase_top line 275
  14. theorem OAI.Erdos3.VectorPolynomial.inhomogeneous_coefficient_mode_local_removal line 295
  15. theorem OAI.Erdos3.VectorPolynomial.inhomogeneous_coefficient_mode_smooth_removal line 342
  16. def OAI.Erdos3.VectorPolynomial.lowerLayerPolynomial line 394
  17. theorem OAI.Erdos3.VectorPolynomial.lowerLayerPolynomial_degree line 400
  18. theorem OAI.Erdos3.VectorPolynomial.lowerLayerPolynomial_eval line 415
  19. def OAI.Erdos3.VectorPolynomial.layeredModeTestedPhase line 426
  20. theorem OAI.Erdos3.VectorPolynomial.exists_layered_mode_reduction line 435
  21. theorem OAI.Erdos3.VectorPolynomial.layeredModeTestedPhase_norm_le line 487
  22. theorem OAI.Erdos3.VectorPolynomial.layered_mode_smooth_removal line 508
  23. theorem OAI.Erdos3.VectorPolynomial.degreeLE_restrictCoefficients line 561
  24. theorem OAI.Erdos3.VectorPolynomial.coefficientModeTestedPhase_map line 567
  25. theorem OAI.Erdos3.VectorPolynomial.layeredModeTestedPhase_map line 576
  26. theorem OAI.Erdos3.VectorPolynomial.exists_subspace_layered_mode_reduction line 587
  27. theorem OAI.Erdos3.VectorPolynomial.subspace_layered_mode_smooth_removal line 624