OAI/NumberTheory/CubicMoment/Theta/CubicThetaPositiveProfileGram.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact finite-row Gram formula for compact Fourier sources, including cutoffs below the injective cusp. The rows and every phase remain literal.

  1. lemma OAI.CubicFirstMoment.cubicThetaFourierProfileTerm_point_continuous line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaPositiveProfileGram_row_integrable line 20
  3. theorem OAI.CubicFirstMoment.cubicThetaPositiveProfileGram_unfold line 28
  4. theorem OAI.CubicFirstMoment.cubicThetaPositiveProfileGram_finite line 39