OAI/Probability/InvariantIsing/Spectral/PositiveResolventFluctuation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform Gaussian mean absolute fluctuations of a normalized resolvent quadratic form.

  1. lemma OAI.InvariantIsing.positiveResolvent_normalized_mean line 11
  2. lemma OAI.InvariantIsing.positiveResolvent_normalized_fluctuation line 18