OAI/NumberTheory/TwoPoint/Bounds/ComplexFullDilation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The full-divisibility part of the complex bin is the exact dilated correlation.

  1. lemma OAI.TwoPointCorrelations.tupleComplexPartialProfile_empty_prefix line 12
  2. lemma OAI.TwoPointCorrelations.fullComplexBin_eq_dilated line 37