OAI/NumberTheory/CubicMoment/Theta/CubicThetaScalarSeedPairing.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Exact periodization of the positive sharp-height seed times section energy.

  1. lemma OAI.CubicFirstMoment.cubicThetaScalarHeightWeight_measurable line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaScalarHeightSeed_measurable line 18
  3. lemma OAI.CubicFirstMoment.cubicThetaSection_norm_invariant line 26
  4. lemma OAI.CubicFirstMoment.cubicThetaScalarRankinKernel_apply line 32
  5. def OAI.CubicFirstMoment.cubicThetaScalarEnergySeed line 41
  6. def OAI.CubicFirstMoment.cubicThetaScalarEnergyDensity line 44
  7. lemma OAI.CubicFirstMoment.cubicThetaScalarEnergySeed_nonneg line 48
  8. lemma OAI.CubicFirstMoment.cubicThetaScalarEnergyDensity_nonneg line 52
  9. lemma OAI.CubicFirstMoment.cubicThetaScalarEnergySeed_measurable line 56
  10. lemma OAI.CubicFirstMoment.cubicThetaScalarEnergyDensity_measurable line 60
  11. lemma OAI.CubicFirstMoment.cubicThetaScalarEnergySeed_group_summable line 65
  12. lemma OAI.CubicFirstMoment.cubicThetaScalarEnergySeed_group_sum line 71