OAI/NumberTheory/TwoPoint/Bounds/PaddingSelectionLaw.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The padding experiment has tilted prime availability 5/(p+4) and, given availability, two independent selections of probability 4/5. Its exact difference pushforward is the manuscript's three-point law.

  1. def OAI.TwoPointCorrelations.booleanLaw line 15
  2. def OAI.TwoPointCorrelations.paddingAvailabilityLaw line 20
  3. def OAI.TwoPointCorrelations.paddingSelectionLaw line 27
  4. def OAI.TwoPointCorrelations.paddingPairLocal line 31
  5. def OAI.TwoPointCorrelations.paddingPairDifference line 35
  6. lemma OAI.TwoPointCorrelations.paddingPairLocal_average line 38
  7. lemma OAI.TwoPointCorrelations.paddingPairLocal_fiber line 50
  8. def OAI.TwoPointCorrelations.paddingPairLaw line 56
  9. lemma OAI.TwoPointCorrelations.paddingPairLaw_average line 60