OAI/Probability/InvariantIsing/Spectral/PositiveResolventEigenbasis.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The positive resolvent in the eigenbasis of the original positive matrix.

  1. lemma OAI.InvariantIsing.positiveResolvent_eigenvector line 12
  2. lemma OAI.InvariantIsing.positiveResolvent_trace_eigenvalues line 35