OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeFourierMode.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Exact action of the finite translation branches on a horizontal Fourier mode with an arbitrary vertical profile. No spectral assertion about the global residue is used here.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeCubeFourierMode line 13
  2. def OAI.CubicFirstMoment.cubicThetaPrimeCubeScaledMode line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeFourierMode_branch line 23
  4. def OAI.CubicFirstMoment.cubicThetaPrimeCubeUnitModeSum line 37
  5. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeUnitModeSum_eq line 44
  6. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeUnitModeSum_zero line 55
  7. def OAI.CubicFirstMoment.cubicThetaPrimeCubeBottomFourier line 62
  8. lemma OAI.CubicFirstMoment.cubicThetaResidues_card_complex line 67
  9. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeBottomFourier_eq line 72