OAI/NumberTheory/CubicMoment/Theta/CubicThetaCuspGreen.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The compact Green operator on all nonzero trace-Fourier cusp modes. The actual lattice norm supplies the finite-mode exhaustion.

  1. abbrev OAI.CubicFirstMoment.CubicThetaNonzeroFrequency line 14
  2. abbrev OAI.CubicFirstMoment.CubicThetaCuspModes line 15
  3. def OAI.CubicFirstMoment.cubicThetaCuspPotential line 17
  4. lemma OAI.CubicFirstMoment.cubicThetaCuspPotential_pos line 20
  5. lemma OAI.CubicFirstMoment.cubicThetaCuspPotential_eq line 24
  6. def OAI.CubicFirstMoment.cubicThetaCuspGreen line 29
  7. lemma OAI.CubicFirstMoment.cubicThetaCuspGreen_apply line 33
  8. lemma OAI.CubicFirstMoment.cubicThetaCuspGreen_norm line 36
  9. lemma OAI.CubicFirstMoment.cubicThetaCuspGreen_small_modes line 39
  10. theorem OAI.CubicFirstMoment.cubicThetaCuspGreen_compact line 67