OAI/NumberTheory/CubicMoment/Estimates/PrimeSubsetNormTail.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The sum over distinct prime subsets has no multiplicity loss after mapping each subset to its primary product. A convergent lattice norm series therefore controls its inverse-square tail.

  1. theorem OAI.CubicFirstMoment.primary_prime_subset_norm_sum line 14
  2. theorem OAI.CubicFirstMoment.primary_prime_subset_harmonic line 28
  3. lemma OAI.CubicFirstMoment.finite_eisenstein_norm_square_tail line 53
  4. theorem OAI.CubicFirstMoment.primary_prime_subset_norm_tail line 68