OAI/NumberTheory/CubicMoment/Theta/CubicThetaCoreBumpIntegral.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The norm of a global core cutoff equals the scalar integral over its actual covering sheet. This retains the cubic section's unit twist.

  1. lemma OAI.CubicFirstMoment.cubicThetaCoreBump_support_image line 14
  2. lemma OAI.CubicFirstMoment.cubicThetaCoreBump_complex_bound line 34
  3. def OAI.CubicFirstMoment.cubicThetaCoreMultiplier line 39
  4. lemma OAI.CubicFirstMoment.cubicThetaCoreMultiplier_ae line 44
  5. def OAI.CubicFirstMoment.cubicThetaCoreMass line 49
  6. lemma OAI.CubicFirstMoment.cubicThetaCoreMass_test_norm_sq line 52
  7. lemma OAI.CubicFirstMoment.cubicThetaCoreMass_sheet_integral line 65