OAI/Probability/Perceptron/Cavity/CavityCovarianceComparison.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.bounded_log_partition_path_derivative line 11
2. def OAI.SphericalPerceptronFreeEnergy.cavityGaussianRotation line 40
3. def OAI.SphericalPerceptronFreeEnergy.cavityGaussianRotationVelocity line 43
4. lemma OAI.SphericalPerceptronFreeEnergy.cavityGaussianRotation_norm line 46
5. lemma OAI.SphericalPerceptronFreeEnergy.cavityGaussianRotationVelocity_norm line 56
6. lemma OAI.SphericalPerceptronFreeEnergy.cavityGaussianRotation_log_derivative line 74
7. lemma OAI.SphericalPerceptronFreeEnergy.cavityGaussianRotation_mean_derivative line 103
8. lemma OAI.SphericalPerceptronFreeEnergy.cavityGaussianRotation_cross_covariance_bound line 151
9. theorem OAI.SphericalPerceptronFreeEnergy.euclideanGaussian_covariance_comparison line 169