OAI/NumberTheory/CubicMoment/Theta/CubicThetaResiduePrimarySupport.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Every nonzero primary residue has genuine squarefree/cube support. Repeated prime cubes are removed by the proved arithmetic periodicity.

  1. lemma OAI.CubicFirstMoment.cubicTheta_primary_cube line 11
  2. theorem OAI.CubicFirstMoment.cubicThetaWeightedFourierResidue_supported line 14
  3. theorem OAI.CubicFirstMoment.cubicThetaWeightedFourierResidue_primary_all line 58