OAI/Probability/Perceptron/Variational/IndexedObservableTransport.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SphericalPerceptronFreeEnergy.indexedHamiltonian_integral_covariance_addition line 15
2. lemma OAI.SphericalPerceptronFreeEnergy.indexedReplicaMean_covariance_addition line 57
3. lemma OAI.SphericalPerceptronFreeEnergy.indexedTiltMean_covariance_addition line 71
4. lemma OAI.SphericalPerceptronFreeEnergy.indexedGaussianRow_right_covariance line 86
5. def OAI.SphericalPerceptronFreeEnergy.indexedResponse line 97
6. lemma OAI.SphericalPerceptronFreeEnergy.indexedResponse_measurable line 102
7. lemma OAI.SphericalPerceptronFreeEnergy.indexedResponse_transport line 119
8. theorem OAI.SphericalPerceptronFreeEnergy.indexedGaussianMean_right_response line 132