OAI/NumberTheory/CubicMoment/Theta/CubicThetaAutomorphicSections.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Continuous sections with the actual cubic multiplier. Their norm descends to the arithmetic quotient, and quotient cutoffs localize them.

  1. def OAI.CubicFirstMoment.cubicThetaAutomorphicSections line 12
  2. abbrev OAI.CubicFirstMoment.CubicThetaSection line 27
  3. def OAI.CubicFirstMoment.cubicThetaSectionNorm line 29
  4. lemma OAI.CubicFirstMoment.cubicThetaSectionNorm_apply line 32
  5. lemma OAI.CubicFirstMoment.cubicThetaSectionNorm_continuous line 39
  6. def OAI.CubicFirstMoment.cubicThetaSectionCutoff line 47
  7. lemma OAI.CubicFirstMoment.cubicThetaSectionCutoff_norm line 57
  8. lemma OAI.CubicFirstMoment.cubicThetaSectionCutoff_compact line 64