OAI/NumberTheory/TwoPoint/Bounds/PaddingSmoothMass.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Averaging smooth-dilation costs under the actual padding divisor law. Only one factor is paid at each selected prime.

  1. lemma OAI.TwoPointCorrelations.smoothReciprocalProduct_selected line 14
  2. lemma OAI.TwoPointCorrelations.padding_smooth_reciprocal_average line 24
  3. lemma OAI.TwoPointCorrelations.padding_smooth_reciprocal_sum line 40