OAI/Probability/InvariantIsing/Gaussian/MPDensityTransform.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The positive resolvent transform of the literal Marchenko--Pastur measure.

  1. lemma OAI.InvariantIsing.mpDensity_measure_integral line 11
  2. theorem OAI.InvariantIsing.marchenkoPastur_transform line 21