OAI/NumberTheory/CubicMoment/Theta/CubicThetaBorelRestriction.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The completed positive-strip restriction is the actual measurable lift from the quotient, including its cubic automorphy factor.

  1. lemma OAI.CubicFirstMoment.cubicThetaPositiveStrip_pull_ae line 13
  2. def OAI.CubicFirstMoment.cubicThetaBorelRestrictionLinear line 23
  3. lemma OAI.CubicFirstMoment.cubicThetaBorelRestrictionLinear_bound line 69
  4. def OAI.CubicFirstMoment.cubicThetaBorelRestriction line 95
  5. lemma OAI.CubicFirstMoment.cubicThetaBorelRestriction_coe line 100
  6. lemma OAI.CubicFirstMoment.cubicThetaBorelRestriction_finite line 106
  7. theorem OAI.CubicFirstMoment.cubicThetaPositiveCuspRestriction_borel line 120
  8. theorem OAI.CubicFirstMoment.cubicThetaResidue_borel_model line 131