OAI/NumberTheory/TwoPoint/Bounds/PaddingIntegerBins.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The squarefree divisor formula uses literal divisibility by the site, including the site zero. Bin membership is exactly the half-open interval condition in the manuscript.

  1. lemma OAI.TwoPointCorrelations.paddingSelectedDivisor_dvd_iff line 15
  2. lemma OAI.TwoPointCorrelations.padding_literal_support_iff_dvd line 33
  3. lemma OAI.TwoPointCorrelations.paddingBin_eq_iff line 42
  4. lemma OAI.TwoPointCorrelations.paddingAvailablePrimes_integer line 46
  5. def OAI.TwoPointCorrelations.integerPaddingBinMass line 59
  6. lemma OAI.TwoPointCorrelations.literalPaddingBinMass_integer line 66
  7. lemma OAI.TwoPointCorrelations.padding_integer_weight_total line 79