OAI/NumberTheory/TwoPoint/Bounds/PaddingBinCount.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Bounds for the actual finite bin set at eta = exp(-J).

  1. lemma OAI.TwoPointCorrelations.paddingBinIndices_card_linear line 12
  2. lemma OAI.TwoPointCorrelations.paddingBinIndices_card_polynomial line 21