OAI/NumberTheory/TwoPoint/Bounds/MatrixSpectralTail.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The exact unnormalized moment controls the exceptional block origins. No self-adjointness of the nonbacktracking matrix is needed.

  1. def OAI.TwoPointCorrelations.realMatrixSpectralRadius line 14
  2. lemma OAI.TwoPointCorrelations.real_matrix_spectral_power_le line 18
  3. theorem OAI.TwoPointCorrelations.FiniteLaw.matrix_spectral_tail line 34
  4. lemma OAI.TwoPointCorrelations.trace_moment_add_one_le line 65
  5. theorem OAI.TwoPointCorrelations.FiniteLaw.matrix_spectral_tail_add_one line 75