OAI/Probability/InvariantIsing/Gaussian/MarchenkoPasturInput.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The Gaussian Marchenko–Pastur theorem, including real spectral scaling.

  1. theorem OAI.InvariantIsing.marchenkoPastur_proved line 11