OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeWeakLift.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual finite-cover trace transports the complete weak energy equation to the prime cover, with all finite-cover test vectors allowed.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeEnergyPencil line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeEnergyPencil_pairing line 16
  3. lemma OAI.CubicFirstMoment.cubicThetaGlobalEnergyPencil_pairing line 25
  4. theorem OAI.CubicFirstMoment.cubicThetaPrimeEnergyPencil_lift_pairing line 32
  5. theorem OAI.CubicFirstMoment.cubicThetaPrimeEnergyPencil_lift_kernel line 39
  6. lemma OAI.CubicFirstMoment.cubicThetaPrimeEnergyPencil_atkin_pairing line 46
  7. theorem OAI.CubicFirstMoment.cubicThetaPrimeEnergyPencil_atkin_kernel line 54