OAI/Probability/Perceptron/Variational/IndexedGaussianCovarianceLaw.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptronFreeEnergy.doubledGaussianRows line 13
2. def OAI.SphericalPerceptronFreeEnergy.diagonalGaussianRows line 17
3. lemma OAI.SphericalPerceptronFreeEnergy.doubledGaussianRows_gram line 20
4. lemma OAI.SphericalPerceptronFreeEnergy.doubledGaussianRows_law line 31
5. lemma OAI.SphericalPerceptronFreeEnergy.doubledGaussianRows_apply line 37
6. lemma OAI.SphericalPerceptronFreeEnergy.diagonalGaussianRows_apply line 43
7. theorem OAI.SphericalPerceptronFreeEnergy.countableGaussian_covariance_addition_law line 50
8. def OAI.SphericalPerceptronFreeEnergy.sharedMarksHamiltonian line 75
9. lemma OAI.SphericalPerceptronFreeEnergy.sharedMarksHamiltonian_measurable line 80
10. lemma OAI.SphericalPerceptronFreeEnergy.sharedMarks_diagonal_eq line 98
11. lemma OAI.SphericalPerceptronFreeEnergy.sharedMarks_doubled_eq line 114
12. theorem OAI.SphericalPerceptronFreeEnergy.indexedGaussianMean_covariance_addition line 134