OAI/Probability/SKBarriers/Replicas/MatrixCovarianceAlgebra.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SK.Analytic.finite_gram_cross_covariance line 15
2. theorem OAI.SK.Analytic.finite_linear_covariance line 40
3. def OAI.SK.Analytic.replicaCrossOverlap line 57
4. def OAI.SK.Analytic.matrixPairFeature line 60
5. theorem OAI.SK.Analytic.matrixPairFeature_covariance line 64
6. def OAI.SK.Analytic.matrixFieldFeature line 81
7. def OAI.SK.Analytic.factorCovariance line 85
8. theorem OAI.SK.Analytic.matrixFieldFeature_covariance line 88