OAI/NumberTheory/JointDickman/Amplification/FourierProfileTail.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Quantitative tail bounds from the fixed Fourier profile's moments

  1. theorem OAI.JointDickman.norm_integral_tail_le_moment line 11
  2. theorem OAI.JointDickman.schwartz_testFourier_tail line 31
  3. theorem OAI.JointDickman.schwartz_testFourier_linear_moment line 37