OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeResidueDefect.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The two missing local-image conditions as bounded functionals of the actual energy space. No vanishing assertion is assumed here.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeFirstDefect line 10
  2. def OAI.CubicFirstMoment.cubicThetaPrimeSecondDefect line 16
  3. def OAI.CubicFirstMoment.cubicThetaPrimeFirstDefectVector line 20
  4. def OAI.CubicFirstMoment.cubicThetaPrimeSecondDefectVector line 23
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeFirstDefectVector_pairing line 26
  6. lemma OAI.CubicFirstMoment.cubicThetaPrimeSecondDefectVector_pairing line 32
  7. theorem OAI.CubicFirstMoment.cubicThetaPrimeDefect_residue_iff line 38
  8. theorem OAI.CubicFirstMoment.cubicThetaPrimeDefectVector_residue_iff line 61