OAI/Probability/Perceptron/Cavity/BulkDeviation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.bulkCouplingSlope_bound line 11
2. lemma OAI.SphericalPerceptronFreeEnergy.bulkCouplingSlope_joint_measurable line 21
3. def OAI.SphericalPerceptronFreeEnergy.bulkSlopeDeviation line 44
4. lemma OAI.SphericalPerceptronFreeEnergy.bulkSlopeDeviation_measurable line 48
5. lemma OAI.SphericalPerceptronFreeEnergy.bulkSlopeDeviation_bound line 54
6. lemma OAI.SphericalPerceptronFreeEnergy.bulkSlopeDeviation_intervalIntegrable line 77
7. lemma OAI.SphericalPerceptronFreeEnergy.bulkLogPartition_fluctuation line 87
8. lemma OAI.SphericalPerceptronFreeEnergy.bulkSlopeDeviation_integrated_bound line 97