OAI/NumberTheory/CubicMoment/Theta/CubicThetaEnergyMellin.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Absolute Fubini for the actual horizontal Fourier energy and its coefficient Dirichlet mass. The frequency dilation is retained exactly.

  1. def OAI.CubicFirstMoment.cubicThetaEnergyMellinTerm line 15
  2. lemma OAI.CubicFirstMoment.cubicThetaEnergyMellinTerm_nonneg line 18
  3. lemma OAI.CubicFirstMoment.cubicThetaEnergyMellinTerm_integrable line 22
  4. lemma OAI.CubicFirstMoment.cubicThetaEnergyMellinTerm_integral line 38
  5. lemma OAI.CubicFirstMoment.cubicThetaEnergyMellinTerm_norm_integral line 63
  6. lemma OAI.CubicFirstMoment.cubicThetaArithmeticFourierEnergy_all line 71
  7. theorem OAI.CubicFirstMoment.cubicThetaArithmeticFourierEnergy_mellin line 83