OAI/NumberTheory/TwoPoint/Walks/CanonicalCorrelationDeletion.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The literal uncut bin correlation differs from the spectral test by the two canonical endpoint deletion costs.

  1. def OAI.TwoPointCorrelations.canonicalUncutPrefix line 15
  2. lemma OAI.TwoPointCorrelations.canonical_uncut_sub_retained_prefix line 22
  3. lemma OAI.TwoPointCorrelations.prefix_start_one_add line 65
  4. lemma OAI.TwoPointCorrelations.canonical_weighted_correlation_deletion line 69