OAI/NumberTheory/TwoPoint/Bounds/PaddingBinCoverage.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The literal finite bin family covers every padding divisor surviving the degree and logarithmic-size cuts. This includes the last bin whose left endpoint, rather than its right endpoint, is at most 100 L.

  1. def OAI.TwoPointCorrelations.paddingBinIndices line 16
  2. lemma OAI.TwoPointCorrelations.mem_paddingBinIndices_iff line 19
  3. lemma OAI.TwoPointCorrelations.paddingBin_mem_indices line 23
  4. lemma OAI.TwoPointCorrelations.paddingBinIndices_card line 31
  5. def OAI.TwoPointCorrelations.PaddingPairEligible line 43
  6. lemma OAI.TwoPointCorrelations.paddingSelectedDivisor_count line 47
  7. lemma OAI.TwoPointCorrelations.padding_pair_eligible_of_retained line 54
  8. lemma OAI.TwoPointCorrelations.reciprocal_padding_eligible_probability line 70
  9. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_padding_bin_probability line 86