OAI/GroupTheory/SimpleAmenable/RandomFields/MatrixDensityCalculus.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SimpleAmenable.determinantMultilinear line 15
2. theorem OAI.SimpleAmenable.determinantMultilinear_apply line 20
3. theorem OAI.SimpleAmenable.matrix_hasDerivAt_det line 23
4. def OAI.SimpleAmenable.noiseGradientCoordinate line 62
5. theorem OAI.SimpleAmenable.singletonNoise_eq line 66
6. theorem OAI.SimpleAmenable.singletonNoise_score line 78
7. theorem OAI.SimpleAmenable.singletonNoise_diagonal line 83
8. theorem OAI.SimpleAmenable.pairNoise_gradient line 91
9. theorem OAI.SimpleAmenable.affineNoiseGenerator_eq line 115
10. theorem OAI.SimpleAmenable.noiseTensor_hasDerivAt line 163