OAI/NumberTheory/TwoPoint/Bounds/ReciprocalPaddingLaw.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The harmonic divisor law 4^omega(q)/(q S) is an actual finite independent prime-selection law with inclusion probabilities 4/(p+4).

  1. def OAI.TwoPointCorrelations.reciprocalPaddingPrimeLaw line 14
  2. def OAI.TwoPointCorrelations.reciprocalPaddingLaw line 19
  3. lemma OAI.TwoPointCorrelations.reciprocal_padding_atom line 22
  4. lemma OAI.TwoPointCorrelations.paddingSelectedDivisor_cast line 30
  5. lemma OAI.TwoPointCorrelations.reciprocal_padding_weight line 35
  6. lemma OAI.TwoPointCorrelations.reciprocal_padding_average line 46
  7. lemma OAI.TwoPointCorrelations.FiniteLaw.independent_average_coordinate line 74
  8. lemma OAI.TwoPointCorrelations.reciprocal_padding_count_average line 86
  9. lemma OAI.TwoPointCorrelations.reciprocal_padding_log_average line 97