OAI/NumberTheory/CubicMoment/Decomposition/DistinguishedPrimeVariation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Actual radial weights when the largest prime lies in a distinguished tuple coordinate. The detector difference has a uniform scaled derivative, so the original smooth weight, rather than an arbitrary bounded sequence, can be used in prime partial summation.

  1. def OAI.CubicFirstMoment.distinguishedRadialWeight line 13
  2. lemma OAI.CubicFirstMoment.detector_difference_smooth line 16
  3. lemma OAI.CubicFirstMoment.detector_difference_norm line 21
  4. lemma OAI.CubicFirstMoment.detector_difference_deriv line 28
  5. theorem OAI.CubicFirstMoment.distinguishedRadialWeight_bounds line 53