OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeRootMassTransport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Fractional translations preserve the literal finite-domain mass and square integrability of cubic-scale automorphic sections.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRootImage_fundamental line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRootSection_norm_invariant line 28
  3. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeRootSectionTranslate_mass line 36
  4. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeRootSectionTranslate_memLp line 49