OAI/NumberTheory/CubicMoment/Theta/CubicThetaArithmeticL2.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The cusp estimates and finite arithmetic core cover put the literal Eisenstein remainder in the actual global L2 space.

  1. lemma OAI.CubicFirstMoment.cubicThetaCuspNeighborhood_integrable_iff line 14
  2. lemma OAI.CubicFirstMoment.cubicThetaArithmeticSection_cusp_mass_integrable line 32
  3. theorem OAI.CubicFirstMoment.cubicThetaArithmeticSection_mass_integrable line 45
  4. lemma OAI.CubicFirstMoment.cubicThetaArithmeticSection_memLp line 60
  5. def OAI.CubicFirstMoment.cubicThetaArithmeticL2 line 67
  6. lemma OAI.CubicFirstMoment.cubicThetaArithmeticL2_coe line 70