OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeLiftL2.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Normalized lifting from the original automorphic L2 closure to the actual finite prime cover. The normalization is the square root of its degree.

  1. def OAI.CubicFirstMoment.cubicThetaGlobalMassClosure line 15
  2. lemma OAI.CubicFirstMoment.cubicThetaGlobalMassClosure_dense line 19
  3. def OAI.CubicFirstMoment.cubicThetaPrimeSmoothRestriction line 32
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeSmoothRestriction_norm_sq line 39
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeCoverDegree_pos line 45
  6. def OAI.CubicFirstMoment.cubicThetaPrimeNormalizedRestriction line 49
  7. lemma OAI.CubicFirstMoment.cubicThetaPrimeNormalizedRestriction_norm line 54
  8. def OAI.CubicFirstMoment.cubicThetaPrimeLiftL2 line 69
  9. lemma OAI.CubicFirstMoment.cubicThetaPrimeLiftL2_smooth line 74