OAI/NumberTheory/TwoPoint/Walks/SelectedRawComparison.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The raw sum for a phase-selected pair family compares to one original correlation, with its actual reciprocal prime cost and a finite boundary term.

  1. def OAI.TwoPointCorrelations.selectedRawMean line 13
  2. def OAI.TwoPointCorrelations.selectedRawCoefficient line 19
  3. lemma OAI.TwoPointCorrelations.selectedRawMean_comparison line 22
  4. lemma OAI.TwoPointCorrelations.selectedRawComparison_cost_bound line 52