OAI/Probability/InvariantIsing/Spectral/SpectralCovariance.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Translation and positive scaling of the finite spectral transform.

  1. theorem OAI.InvariantIsing.finiteInverse_constant line 15
  2. theorem OAI.InvariantIsing.finiteR_constant line 23
  3. theorem OAI.InvariantIsing.finiteResolvent_scale line 32
  4. theorem OAI.InvariantIsing.finiteInverse_translate line 42
  5. theorem OAI.InvariantIsing.finiteInverse_scale line 52
  6. theorem OAI.InvariantIsing.finiteR_translate line 63
  7. theorem OAI.InvariantIsing.finiteR_scale line 74