OAI/NumberTheory/TwoPoint/Walks/SelectedBinEligibility.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A numerical phase selection gives an admissible graph eligibility in each actual logarithmic bin, including the padding degree restriction.

  1. def OAI.TwoPointCorrelations.selectedPairBin line 14
  2. lemma OAI.TwoPointCorrelations.selectedPairBin_properties line 18
  3. lemma OAI.TwoPointCorrelations.selectedPairBin_index line 37
  4. lemma OAI.TwoPointCorrelations.selected_pairs_bounded_padding line 43