OAI/NumberTheory/TwoPoint/Bounds/NumericalBins.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

One common eligibility predicate for the literal manuscript bins. Positivity makes the log-product identity valid even outside the prime pools.

  1. def OAI.TwoPointCorrelations.numericalBinEligible line 15
  2. lemma OAI.TwoPointCorrelations.numericalBinEligible_bin line 19
  3. lemma OAI.TwoPointCorrelations.numericalBinEligible_pair line 22
  4. lemma OAI.TwoPointCorrelations.numericalBin_mass line 37