OAI/Probability/Perceptron/Cavity/CavityResidualUncap.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.cavity_residual_square_integrable line 12
2. lemma OAI.SphericalPerceptronFreeEnergy.cavity_expected_cap_residual line 51
3. def OAI.SphericalPerceptronFreeEnergy.cavityLabelCompletedMark line 68
4. lemma OAI.SphericalPerceptronFreeEnergy.cavityLabelCompletedMark_measurable line 74
5. def OAI.SphericalPerceptronFreeEnergy.cavityLabelSpherical line 91
6. def OAI.SphericalPerceptronFreeEnergy.cavityLabelWeight line 95
7. lemma OAI.SphericalPerceptronFreeEnergy.cavityLabelSpherical_measurable line 99
8. lemma OAI.SphericalPerceptronFreeEnergy.cavityLabelWeight_measurable line 105
9. lemma OAI.SphericalPerceptronFreeEnergy.cavityLabelWeight_bound line 113
10. lemma OAI.SphericalPerceptronFreeEnergy.cavityLabelSpherical_one line 121
11. lemma OAI.SphericalPerceptronFreeEnergy.cavityLabelSpherical_second line 125
12. theorem OAI.SphericalPerceptronFreeEnergy.cavityLabel_cap_error line 156