OAI/NumberTheory/TwoPoint/Bounds/GraphMatrixCompression.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The real integer-edge matrix, its complex graph operator, and the nonbacktracking block have exactly the same spectral parameter.

  1. def OAI.TwoPointCorrelations.primeRealEdgeMatrix line 14
  2. lemma OAI.TwoPointCorrelations.primeFamilyGraphOperator_eq_realMatrix line 24
  3. theorem OAI.TwoPointCorrelations.prime_graph_compression_of_matrix_radius line 46