OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeRootStripBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A literal cusp strip has at most one representative in each orbit of any subgroup of the principal group. Its mass is bounded by fundamental-domain mass, also for the cubic-root cover.

  1. lemma OAI.CubicFirstMoment.cubicThetaInjective_subgroup_disjoint line 15
  2. lemma OAI.CubicFirstMoment.cubicThetaInjective_subgroup_lintegral_le line 33
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRoot_strip_lintegral_le line 49
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRoot_strip_memLp line 60