OAI/NumberTheory/CubicMoment/Estimates/HeightConvolution.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Absolute Fubini for a bounded height polynomial and an integrable Mellin weight. No mean estimate or interchange is assumed.

  1. lemma OAI.CubicFirstMoment.continuous_height_convolution line 12
  2. lemma OAI.CubicFirstMoment.integrable_height_convolution_kernel line 27
  3. lemma OAI.CubicFirstMoment.height_convolution_interval_swap line 57
  4. lemma OAI.CubicFirstMoment.integrable_height_convolution_interval line 70
  5. lemma OAI.CubicFirstMoment.intervalIntegrable_height_convolution line 79
  6. theorem OAI.CubicFirstMoment.dyadicHeightMean_convolution line 86