OAI/Probability/Perceptron/Pressure/VectorPartition.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptronFreeEnergy.vectorPartition line 18
2. def OAI.SphericalPerceptronFreeEnergy.vectorLogPartition line 21
3. def OAI.SphericalPerceptronFreeEnergy.vectorLogDerivative line 24
4. lemma OAI.SphericalPerceptronFreeEnergy.vectorEnergy_bound line 28
5. lemma OAI.SphericalPerceptronFreeEnergy.vectorPartition_integrable line 36
6. lemma OAI.SphericalPerceptronFreeEnergy.vectorPartition_pos line 44
7. lemma OAI.SphericalPerceptronFreeEnergy.vectorPartition_hasFDerivAt line 52
8. lemma OAI.SphericalPerceptronFreeEnergy.vectorLogPartition_hasFDerivAt line 74
9. lemma OAI.SphericalPerceptronFreeEnergy.vectorLogDerivative_bound line 81
10. lemma OAI.SphericalPerceptronFreeEnergy.vectorLogDerivative_continuous line 99
11. lemma OAI.SphericalPerceptronFreeEnergy.vectorLogPartition_gaussian_variance line 123