OAI/NumberTheory/CubicMoment/Estimates/LargeTupleWeights.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

A single uniform smooth family for the actual distinguished-prime weights in each large-row norm piece. Both scale ratios are capped only after proving that the cap leaves the weight unchanged.

  1. def OAI.CubicFirstMoment.distinguishedSmoothWeight line 14
  2. lemma OAI.CubicFirstMoment.distinguishedSmoothWeight_low line 17
  3. lemma OAI.CubicFirstMoment.distinguishedSmoothWeight_high line 21
  4. lemma OAI.CubicFirstMoment.distinguishedSmoothWeight_norm line 25
  5. lemma OAI.CubicFirstMoment.distinguishedSmoothWeight_capped line 40
  6. lemma OAI.CubicFirstMoment.distinguishedSmoothWeight_contDiff line 45
  7. lemma OAI.CubicFirstMoment.distinguishedSmoothWeight_support line 62
  8. def OAI.CubicFirstMoment.compactDistinguishedSmoothWeights line 70
  9. def OAI.CubicFirstMoment.distinguishedSmoothWeights line 77
  10. lemma OAI.CubicFirstMoment.distinguishedSmoothWeight_at_prime line 93
  11. def OAI.CubicFirstMoment.largePrimeSmoothWeight line 106
  12. def OAI.CubicFirstMoment.largePrimeSmoothWeights line 110