OAI/Probability/InvariantIsing/Gaussian/GaussianGramResolvent.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The positive real resolvent of the physical Gaussian Gram matrix.

  1. def OAI.InvariantIsing.gaussianGramResolvent line 11
  2. def OAI.InvariantIsing.gaussianGramStieltjes line 15
  3. lemma OAI.InvariantIsing.gaussianPatternCoupling_posSemidef line 18
  4. lemma OAI.InvariantIsing.gaussianGramShift_posDef line 24
  5. lemma OAI.InvariantIsing.gaussianGramResolvent_posDef line 29
  6. lemma OAI.InvariantIsing.gaussianGramResolvent_identity line 33
  7. lemma OAI.InvariantIsing.gaussianGramResolvent_trace_identity line 41
  8. lemma OAI.InvariantIsing.gaussianGramStieltjes_nonneg line 48