OAI/NumberTheory/CubicMoment/Theta/CubicThetaInversionRestriction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The literal inverted cusp restriction extends continuously from finite-energy sections and agrees with inversion on the energy completion.

  1. lemma OAI.CubicFirstMoment.cubicThetaInvertedFiniteRestriction_energy_bound line 11
  2. def OAI.CubicFirstMoment.cubicThetaInvertedFiniteExtension line 18
  3. lemma OAI.CubicFirstMoment.cubicThetaInvertedFiniteExtension_finite line 23
  4. lemma OAI.CubicFirstMoment.cubicThetaInvertedFiniteExtension_test line 30
  5. theorem OAI.CubicFirstMoment.cubicThetaInvertedFiniteExtension_eq line 41
  6. theorem OAI.CubicFirstMoment.cubicThetaCuspRestriction_inversion_finite line 49