OAI/NumberTheory/CubicMoment/Decomposition/PrimeProductDetector.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Apply the manuscript's exact prime detector to the actual central integral kernel. The support is a concrete subset of the primary lattice, with both norm endpoints enforced before the detector is invoked.

  1. lemma OAI.CubicFirstMoment.primeProductEnvelope_zero_lower line 15
  2. def OAI.CubicFirstMoment.primeProductSupport line 23
  3. lemma OAI.CubicFirstMoment.primeProductSupport_spec line 26
  4. lemma OAI.CubicFirstMoment.primeProductLowHeight_support line 33
  5. def OAI.CubicFirstMoment.centralRoughProduct line 56
  6. def OAI.CubicFirstMoment.centralSemiprimeProduct line 61
  7. theorem OAI.CubicFirstMoment.primeProductLowHeight_detector line 66