OAI/Probability/Perceptron/Cavity/CavityExpectedCompensator.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptronFreeEnergy.bulkCDefect line 11
2. lemma OAI.SphericalPerceptronFreeEnergy.bulkCDefect_measurable line 16
3. lemma OAI.SphericalPerceptronFreeEnergy.bulkCDefect_bound line 21
4. lemma OAI.SphericalPerceptronFreeEnergy.bulkCDefect_integral line 32
5. def OAI.SphericalPerceptronFreeEnergy.cavityBulkCompError line 44
6. lemma OAI.SphericalPerceptronFreeEnergy.cavityBulkCompError_measurable line 49
7. lemma OAI.SphericalPerceptronFreeEnergy.cavityBulkCompError_integrable line 54
8. lemma OAI.SphericalPerceptronFreeEnergy.cavityBulkCompError_mean_bound line 68
9. theorem OAI.SphericalPerceptronFreeEnergy.cavityBulkCompError_tendsto_zero line 88