OAI/NumberTheory/CubicMoment/Theta/CubicThetaPositiveFourierMass.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

All positive-cutoff Fourier profiles lie in the actual mass closure. Their pairings are the full positive-height Fourier integrals.

  1. lemma OAI.CubicFirstMoment.cubicThetaPositiveRadialIntegral_zero_extension line 14
  2. lemma OAI.CubicFirstMoment.cubicThetaPositiveRadialIntegral_integrable line 26
  3. def OAI.CubicFirstMoment.cubicThetaPositiveFourierMass line 45
  4. lemma OAI.CubicFirstMoment.cubicThetaPositiveFourierMass_pairing_finite line 50
  5. lemma OAI.CubicFirstMoment.cubicThetaPositiveFourier_integrable line 60
  6. lemma OAI.CubicFirstMoment.cubicThetaRadialWeightScale_positive_low line 67