OAI/NumberTheory/TwoPoint/Bounds/VariableWindowComparison.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite families of interval comparisons may use a different integer length in every bin. No common probability space for the sampled integer intervals is needed.

  1. lemma OAI.TwoPointCorrelations.finite_interval_family_error line 13
  2. lemma OAI.TwoPointCorrelations.finset_sum_error line 23