OAI/NumberTheory/TwoPoint/Walks/BlockOperatorSpectrum.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Identify the concrete nonbacktracking matrix with the operator in the spectral transfer lemma. The change of norm is by conjugacy.

  1. def OAI.TwoPointCorrelations.blockEuclideanEquiv line 16
  2. lemma OAI.TwoPointCorrelations.blockEuclideanEquiv_apply line 27
  3. lemma OAI.TwoPointCorrelations.blockEuclideanEquiv_symm_apply line 31
  4. lemma OAI.TwoPointCorrelations.blockNonbacktracking_operator_conj line 34
  5. theorem OAI.TwoPointCorrelations.blockNonbacktracking_spectralRadius line 57