OAI/NumberTheory/CubicMoment/Decomposition/PrimeProductEnvelope.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

A fixed smooth product envelope equals one on the full sharp dyadic interval. Thus the exact prime cutoff can be retained in the height integral while every factorized row has a smooth product weight.

  1. def OAI.CubicFirstMoment.primeProductBump line 14
  2. def OAI.CubicFirstMoment.primeProductEnvelope line 20
  3. lemma OAI.CubicFirstMoment.primeProductEnvelope_tsupport line 22
  4. lemma OAI.CubicFirstMoment.primeProductEnvelope_compact line 28
  5. lemma OAI.CubicFirstMoment.primeProductEnvelope_positive line 33
  6. lemma OAI.CubicFirstMoment.primeProductEnvelope_smooth line 42
  7. def OAI.CubicFirstMoment.primeProductWeights line 45
  8. lemma OAI.CubicFirstMoment.primeProductEnvelope_norm_le line 49
  9. lemma OAI.CubicFirstMoment.primeProductEnvelope_one line 53
  10. lemma OAI.CubicFirstMoment.primeProductEnvelope_zero line 62
  11. lemma OAI.CubicFirstMoment.primeProductEnvelope_sharp line 69
  12. lemma OAI.CubicFirstMoment.sharpDyadicPrimeComparison_envelope line 79
  13. lemma OAI.CubicFirstMoment.primeProductComparison_bound line 89