OAI/Probability/InvariantIsing/Spectral/PositiveResolventVariance.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The dimension-explicit Gaussian quadratic variance bound for a positive resolvent.

  1. lemma OAI.InvariantIsing.positiveResolvent_quadratic_variance line 11
  2. lemma OAI.InvariantIsing.positiveResolvent_normalized_variance line 26