OAI/NumberTheory/CubicMoment/Estimates/PrimeDyadicReconstruction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual prime sums satisfy the small-argument and local-growth conditions of dyadic reconstruction; closed interval endpoints cost O(1).

  1. def OAI.CubicFirstMoment.primeDyadicSum line 13
  2. lemma OAI.CubicFirstMoment.primeCutoffSum_on line 16
  3. lemma OAI.CubicFirstMoment.primeCutoffSum_zero_small line 28
  4. lemma OAI.CubicFirstMoment.primeCutoffSum_norm_le line 37
  5. lemma OAI.CubicFirstMoment.prime_norm_boundary_sum_le line 53
  6. lemma OAI.CubicFirstMoment.prime_dyadic_endpoint_identity line 72
  7. lemma OAI.CubicFirstMoment.prime_dyadic_endpoint_bound line 98