OAI/NumberTheory/CubicMoment/Theta/CubicThetaFourierMass.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Smooth compact Fourier sources in the genuine automorphic mass closure, and the adjoint link to the completed energy space.

  1. def OAI.CubicFirstMoment.cubicThetaHighFourierMass line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaHighFourierMass_val line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaHighFourierMass_pairing line 21
  4. lemma OAI.CubicFirstMoment.cubicThetaHighFourierMass_orthogonal line 29
  5. lemma OAI.CubicFirstMoment.cubicThetaIntertwining_adjoint line 36
  6. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeMass_adjoint_energy line 48