OAI/Probability/Perceptron/Cavity/CavityOldExpectation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.cavity_three_integral line 12
2. lemma OAI.SphericalPerceptronFreeEnergy.cavity_three_integral_compare line 22
3. def OAI.SphericalPerceptronFreeEnergy.cavityOldError line 45
4. lemma OAI.SphericalPerceptronFreeEnergy.cavitySplitLog_proxy_integrable line 56
5. lemma OAI.SphericalPerceptronFreeEnergy.cavity_proxy_conditional_lower line 70
6. lemma OAI.SphericalPerceptronFreeEnergy.cavity_proxy_expected_lower line 91
7. lemma OAI.SphericalPerceptronFreeEnergy.cavity_actual_proxy_log_bound line 116
8. lemma OAI.SphericalPerceptronFreeEnergy.cavityFreshProjection_preserving line 143
9. lemma OAI.SphericalPerceptronFreeEnergy.cavity_fresh_expected_lower line 157