OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeRootBruhatL2.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact unit-branch transport on the cubic-scale Hilbert completion. There is no arithmetic-residue or Hecke-eigenvector hypothesis here.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRootWeyl_translated_global line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRootFinite_bruhat line 30
  3. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeRootWeyl_mass_bruhat line 39
  4. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeRoot_unit_correlation line 57
  5. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeRoot_unit_residue_correlation line 75