OAI/Probability/Perceptron/Cavity/CavityGaussianQuadratic.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptronFreeEnergy.squareGaussianVariance line 11
2. lemma OAI.SphericalPerceptronFreeEnergy.squareGaussianVariance_nonneg line 13
3. lemma OAI.SphericalPerceptronFreeEnergy.gaussian_square_variance_scale line 15
4. def OAI.SphericalPerceptronFreeEnergy.cavityQuadraticScalar line 26
5. lemma OAI.SphericalPerceptronFreeEnergy.cavityQuadraticScalar_memLp line 29
6. lemma OAI.SphericalPerceptronFreeEnergy.cavityQuadraticScalar_mean line 35
7. lemma OAI.SphericalPerceptronFreeEnergy.cavityQuadraticScalar_second_moment line 49
8. lemma OAI.SphericalPerceptronFreeEnergy.cavityQuadraticScalar_second_moment_bound line 67