OAI/NumberTheory/TwoPoint/Bounds/ComplexNumericalPrefix.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Numerical divisor reindexing of the arbitrary complex retained prefix.

  1. def OAI.TwoPointCorrelations.untwistedRetainedPrefix line 14
  2. def OAI.TwoPointCorrelations.untwistedUncutPrefix line 23
  3. lemma OAI.TwoPointCorrelations.retainedComplex_row_eq_numerical line 30
  4. lemma OAI.TwoPointCorrelations.retainedComplexPrefix_eq_numerical line 62
  5. lemma OAI.TwoPointCorrelations.untwistedRetainedPrefix_congr_eligible line 81