OAI/Probability/SKGap/Gaussian/GaussianSign.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SKGap.gaussianSignEquivline 12 - lemma
OAI.SKGap.gaussianSign_mapline 21 - lemma
OAI.SKGap.gaussianSign_integralline 32 - def
OAI.SKGap.goeSignline 39 - lemma
OAI.SKGap.goeSign_sqline 43 - lemma
OAI.SKGap.goeMatrix_signline 50 - lemma
OAI.SKGap.goe_equivariant_offdiagline 58