OAI/NumberTheory/CubicMoment/Theta/CubicThetaFourierProfilePairing.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Compact Fourier Poincare profiles realize the adjoint cusp observations as actual global L2 functions.

  1. lemma OAI.CubicFirstMoment.cubicThetaFourierProfileSeries_off_cusp line 13
  2. def OAI.CubicFirstMoment.cubicThetaFourierProfileL2 line 32
  3. lemma OAI.CubicFirstMoment.cubicThetaFourierProfilePairing_section line 37
  4. lemma OAI.CubicFirstMoment.cubicThetaFourierProfilePairing_finiteEnergy line 68
  5. theorem OAI.CubicFirstMoment.cubicThetaFourierProfilePairing_energy line 82
  6. theorem OAI.CubicFirstMoment.cubicThetaFourierProfileL2_adjoint line 93