OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeDoubleRootTranslationIntegral.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Nontrivial translations at the intermediate denominator have zero integral correlation, by the proved Bruhat identity and character cancellation.

  1. theorem OAI.CubicFirstMoment.cubicThetaPrimeDoubleRootWeyl_translated_global line 13
  2. theorem OAI.CubicFirstMoment.cubicThetaPrimeDoubleRoot_translation_integral_zero line 30