OAI/NumberTheory/CubicMoment/Theta/CubicThetaHighWindowPairing.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The global pairing with the high forcing is exactly the constant cusp observation, first on actual sections and then on the energy closure.

  1. lemma OAI.CubicFirstMoment.cubicThetaHighWindowSeries_off_cusp line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaInjective_complex_integral line 30
  3. def OAI.CubicFirstMoment.cubicThetaHighWindowL2 line 38
  4. lemma OAI.CubicFirstMoment.cubicThetaHighWindowPairing_section line 42
  5. lemma OAI.CubicFirstMoment.cubicThetaHighWindowPairing_finiteEnergy line 70
  6. theorem OAI.CubicFirstMoment.cubicThetaHighWindowPairing_energy line 84
  7. theorem OAI.CubicFirstMoment.cubicThetaHighWindowPairing_residue_zero_closed line 106
  8. theorem OAI.CubicFirstMoment.cubicThetaHighWindowPairing_residue_zero line 114