OAI/NumberTheory/TwoPoint/Bounds/ComplexCanonicalDeletion.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual complex uncut correlation is controlled by the existing two endpoint costs.

  1. def OAI.TwoPointCorrelations.canonicalComplexUncutPrefix line 14
  2. lemma OAI.TwoPointCorrelations.canonical_complex_uncut_sub_retained_prefix line 21
  3. lemma OAI.TwoPointCorrelations.canonical_complex_weighted_correlation_deletion line 67