OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeRootRestrictionL2.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The original automorphic L2 norm acquires exactly the finite-cover degree under restriction to the root cover.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootSectionRestrict_memLp line 13
  2. theorem OAI.CubicFirstMoment.cubicThetaPrimeRootSectionRestrict_L2_norm_sq line 29