OAI/NumberTheory/TwoPoint/Bounds/PositiveCostPeriodicity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Periodicity needed to shift each numerical pair separately before averaging its nonnegative deletion cost.

  1. lemma OAI.TwoPointCorrelations.ProhibitedPrimeFamily.paddingRejectionAtom_congr line 14
  2. lemma OAI.TwoPointCorrelations.ProhibitedPrimeFamily.padding_rejection_average_translate line 31
  3. lemma OAI.TwoPointCorrelations.ProhibitedPrimeFamily.prohibited_cost_average_translate line 43