OAI/NumberTheory/TwoPoint/Walks/RetainedBinSummation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Sum the retained bin estimates and divide by the retained harmonic mass. No extra factor is hidden in the mass normalization.

  1. lemma OAI.TwoPointCorrelations.retained_bin_sum_normalize line 14
  2. lemma OAI.TwoPointCorrelations.retained_bin_sum_mass_lower line 33