OAI/NumberTheory/CubicMoment/Estimates/RestrictedPrimeTuples.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact tuple collection with an arbitrary original product restriction. This allows the large distinguished rows to retain their sharp support when both convolutions are expanded.

  1. lemma OAI.CubicFirstMoment.orderedConvolution_sum_restrict line 15
  2. lemma OAI.CubicFirstMoment.orderedConvolution_double_restrict line 35