OAI/NumberTheory/TwoPoint/Bounds/FullNumericalBins.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The full-divisibility main term on the exact retained numerical pairs, with its original harmonic mass and real bin endpoint.

  1. def OAI.TwoPointCorrelations.numericalBinPairs line 14
  2. def OAI.TwoPointCorrelations.numericalBinHarmonicMass line 17
  3. def OAI.TwoPointCorrelations.fullNumericalBin line 20
  4. lemma OAI.TwoPointCorrelations.numericalBinHarmonicMass_nonneg line 25
  5. lemma OAI.TwoPointCorrelations.fullNumericalBin_error line 31
  6. lemma OAI.TwoPointCorrelations.numericalBinHarmonicMass_total line 57
  7. theorem OAI.TwoPointCorrelations.fullNumericalBins_error line 66