OAI/NumberTheory/TwoPoint/ShortIntervals/MRTSparsePolynomial.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The sparse Gram bound for the actual finite exponential polynomial. The optional nonnegative weight permits a smooth integer majorant.

  1. theorem OAI.TwoPointCorrelations.mrt_sparse_polynomial_energy line 13
  2. theorem OAI.TwoPointCorrelations.mrt_sparse_weighted_polynomial_energy line 36