OAI/NumberTheory/CubicMoment/Theta/CubicThetaPositiveFourierSmooth.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Smooth positive-cutoff Fourier profiles are actual compact smooth sections, hence belong to the automorphic energy and mass spaces.

  1. lemma OAI.CubicFirstMoment.cubicThetaHorizontalCharacter_contDiff line 14
  2. lemma OAI.CubicFirstMoment.cubicThetaFourierProfileTerm_contDiffAt line 24
  3. lemma OAI.CubicFirstMoment.cubicThetaPositiveFourierProfile_contDiffOn line 33
  4. def OAI.CubicFirstMoment.cubicThetaPositiveFourierProfileTest line 47
  5. lemma OAI.CubicFirstMoment.cubicThetaPositiveFourierProfileL2_mem line 61