OAI/NumberTheory/CubicMoment/Estimates/HeightPolynomialIntegral.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact interchange between finite height Fourier coefficients and the actual norm polynomial. No frequency truncation is used.

  1. lemma OAI.CubicFirstMoment.height_norm_phase line 13
  2. lemma OAI.CubicFirstMoment.integrable_height_phase line 22
  3. theorem OAI.CubicFirstMoment.height_norm_polynomial_integral line 29