OAI/NumberTheory/CubicMoment/Estimates/SemiprimeGaussTailAngularWeights.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Actual semiprime coordinates as a uniform smooth prime-weight family. The angular factor remains separate from the radial weight throughout.

  1. abbrev OAI.CubicFirstMoment.SemiprimeAngularWeightParameters line 13
  2. def OAI.CubicFirstMoment.semiprimeAngularLeftLength line 16
  3. def OAI.CubicFirstMoment.semiprimeAngularRightLength line 18
  4. def OAI.CubicFirstMoment.semiprimeAngularLeftWeight line 20
  5. def OAI.CubicFirstMoment.semiprimeAngularRightWeight line 23
  6. def OAI.CubicFirstMoment.semiprimeAngularLeftLogWeights line 26
  7. def OAI.CubicFirstMoment.semiprimeAngularRightLogWeights line 34
  8. def OAI.CubicFirstMoment.semiprimeAngularUnitPolynomial line 42
  9. lemma OAI.CubicFirstMoment.semiprimeAngularGaussPolynomial_eq_unit line 49