OAI/NumberTheory/TwoPoint/Bounds/PrimeComplexMatrix.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The canonical tuple graph has the same retained real kernel for all bounded tests.

  1. def OAI.TwoPointCorrelations.retainedPrimeMatrix line 14
  2. theorem OAI.TwoPointCorrelations.prime_graph_retained_bilinear line 23
  3. lemma OAI.TwoPointCorrelations.projectedComplexVector_eq line 71
  4. theorem OAI.TwoPointCorrelations.projected_prime_complex_bilinear line 80