OAI/NumberTheory/CubicMoment/Estimates/SemiprimeSmoothWeights.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The roughness transition in each actual semiprime norm piece belongs to a single uniform smooth family. Capping its scale ratio at two is an identity on the fixed norm support, so all logarithmic derivatives are uniform even when the original ratio is unbounded.

  1. def OAI.CubicFirstMoment.semiprimeSmoothWeight line 16
  2. lemma OAI.CubicFirstMoment.semiprimeSmoothWeight_low line 19
  3. lemma OAI.CubicFirstMoment.semiprimeSmoothWeight_high line 23
  4. lemma OAI.CubicFirstMoment.semiprimeSmoothWeight_norm line 27
  5. lemma OAI.CubicFirstMoment.semiprimeSmoothWeight_capped line 38
  6. def OAI.CubicFirstMoment.semiprimeSmoothWeights line 51
  7. lemma OAI.CubicFirstMoment.semiprimeSmoothWeight_at_prime line 74