OAI/Probability/SphericalField/Gibbs/RootVariance.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptron.vectorPartition line 23
2. def OAI.SphericalPerceptron.vectorLogPartition line 26
3. def OAI.SphericalPerceptron.vectorLogDerivative line 29
4. lemma OAI.SphericalPerceptron.vectorEnergy_bound line 33
5. lemma OAI.SphericalPerceptron.vectorPartition_integrable line 41
6. lemma OAI.SphericalPerceptron.vectorPartition_pos line 49
7. lemma OAI.SphericalPerceptron.vectorPartition_hasFDerivAt line 57
8. lemma OAI.SphericalPerceptron.vectorLogPartition_hasFDerivAt line 79
9. lemma OAI.SphericalPerceptron.vectorLogDerivative_bound line 86
10. lemma OAI.SphericalPerceptron.vectorLogDerivative_continuous line 104
11. lemma OAI.SphericalPerceptron.vectorLogPartition_gaussian_variance line 128