OAI/NumberTheory/TwoPoint/Bounds/PartialCenteringSum.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact finite summation of partial-centering errors. Each removed supply subset costs its retained reciprocal mass, never its number of primes.

  1. lemma OAI.TwoPointCorrelations.positivePrefix_sum_finite line 14
  2. lemma OAI.TwoPointCorrelations.tupleCenteredProfile_nonraw_prefix line 20
  3. lemma OAI.TwoPointCorrelations.complement_product_le line 43
  4. lemma OAI.TwoPointCorrelations.partial_centering_sum_bound line 49