OAI/NumberTheory/CubicMoment/Estimates/CoprimeMellinMass.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The divisor expansion of the actual radial kernel is bounded by its literal character-row masses. This keeps the oscillation that is lost in the coarse operator norm bound.

  1. lemma OAI.CubicFirstMoment.finite_bilinear_mass_bound line 14
  2. def OAI.CubicFirstMoment.coprimeMellinMass line 29
  3. theorem OAI.CubicFirstMoment.norm_coprimeMellinKernel_le_mass line 37