OAI/NumberTheory/CubicMoment/Estimates/PrimeSliceEnergySum.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Sum the shortened coefficient energies over common divisors without paying for the ambient prime set. Each n-fold prime product has at most 2^n subsets of prime divisors.

  1. lemma OAI.CubicFirstMoment.fullPrime_divisor_energy_eq_slice line 16
  2. lemma OAI.CubicFirstMoment.fullPrime_summed_slice_energy line 27