OAI/Probability/Perceptron/Cavity/CavityGoodFreshLower.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.cavity_good_fresh_fullLog_lower line 13
2. def OAI.SphericalPerceptronFreeEnergy.cavityOriginalIncrement line 38
3. lemma OAI.SphericalPerceptronFreeEnergy.cavity_original_increment_error line 42
4. lemma OAI.SphericalPerceptronFreeEnergy.cavity_original_increment_background line 71
5. lemma OAI.SphericalPerceptronFreeEnergy.cavity_original_increment_good line 94
6. lemma OAI.SphericalPerceptronFreeEnergy.bulkExpectedLog_parameter_measurable line 116
7. lemma OAI.SphericalPerceptronFreeEnergy.bulkExpectedLog_box_bound line 125
8. lemma OAI.SphericalPerceptronFreeEnergy.bulkExpectedLog_parameter_integrable line 146
9. def OAI.SphericalPerceptronFreeEnergy.cavityAveragedLog line 154
10. lemma OAI.SphericalPerceptronFreeEnergy.cavityAveragedLog_sub line 157
11. lemma OAI.SphericalPerceptronFreeEnergy.integral_good_bad_lower line 163
12. lemma OAI.SphericalPerceptronFreeEnergy.cavity_averaged_increment_good line 180