OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCriticalMatrix.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The finite three-class matrix built from the critical geometric shell sums and the two cubic Gauss factors. This proves the algebraic rank-one calculation in the tame cubic case of Deligne, Bourbaki 539, §§6.5--6.7. Its identification with the local action on the global residue is separate.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeCriticalShellSum line 15
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeCriticalShellSum_eq line 18
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeCriticalShellSum_cancel line 25
  4. def OAI.CubicFirstMoment.cubicThetaPrimeCriticalMatrix line 35
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeCriticalMatrix_eq line 43
  6. lemma OAI.CubicFirstMoment.cubicThetaPrimeCriticalMatrix_mulVec line 52
  7. lemma OAI.CubicFirstMoment.cubicThetaPrimeCriticalMatrix_range_relation line 61
  8. theorem OAI.CubicFirstMoment.cubicThetaPrimeCriticalMatrix_range_iff line 73