OAI/Probability/Perceptron/Cavity/BulkParameterDeviation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.bulkFeature_joint_continuous line 12
2. lemma OAI.SphericalPerceptronFreeEnergy.bulkHamiltonian_parameter_continuous line 26
3. def OAI.SphericalPerceptronFreeEnergy.bulkDegreeDeviation line 34
4. lemma OAI.SphericalPerceptronFreeEnergy.bulkDegreeDeviation_measurable line 37
5. lemma OAI.SphericalPerceptronFreeEnergy.bulkDegreeDeviation_nonneg line 58
6. lemma OAI.SphericalPerceptronFreeEnergy.bulkDegreeDeviation_integrable line 61
7. lemma OAI.SphericalPerceptronFreeEnergy.bulkDegreeDeviation_update line 69
8. lemma OAI.SphericalPerceptronFreeEnergy.bulkDegreeDeviation_integral_bound line 73