OAI/NumberTheory/CubicMoment/Estimates/FullPrimeSliceMoments.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Shortened energies and all three sieve orientations for the literal quotient coefficients β(fn). These are used for common-factor tails.

  1. def OAI.CubicFirstMoment.fullPrimeSliceSum line 14
  2. lemma OAI.CubicFirstMoment.fullPrime_slice_twisted_energy line 19
  3. theorem OAI.CubicFirstMoment.logarithmic_full_slice_energy line 31