OAI/NumberTheory/CubicMoment/Estimates/IndependentMellinTail.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The high-coordinate tail of the genuine product Mellin weight is bounded by its explicit finite sum of coordinate moments.

  1. def OAI.CubicFirstMoment.mellinHeightBox line 13
  2. def OAI.CubicFirstMoment.mellinHeightPower line 15
  3. lemma OAI.CubicFirstMoment.measurableSet_mellinHeightBox line 18
  4. lemma OAI.CubicFirstMoment.mellinHeightPower_nonneg line 26
  5. lemma OAI.CubicFirstMoment.mellinHeightPower_large line 30
  6. theorem OAI.CubicFirstMoment.multivariate_weighted_tail line 39
  7. lemma OAI.CubicFirstMoment.prod_one_coordinate line 52
  8. lemma OAI.CubicFirstMoment.independentMellinWeight_coordinate_moment_integrable line 61
  9. lemma OAI.CubicFirstMoment.independentMellinWeight_moment_integrable line 84
  10. lemma OAI.CubicFirstMoment.independentMellinWeight_norm_scale line 94
  11. def OAI.CubicFirstMoment.independentMellinMoment line 103
  12. lemma OAI.CubicFirstMoment.independentMellinMoment_nonneg line 107
  13. lemma OAI.CubicFirstMoment.independentMellinWeight_moment line 112
  14. theorem OAI.CubicFirstMoment.independentMellinWeight_tail line 119