OAI/Probability/Perceptron/Cavity/CavityExpectedQDrop.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.cavityQuadraticField_abs_bound line 12
2. lemma OAI.SphericalPerceptronFreeEnergy.cavity_log_integrable_of_bound line 35
3. lemma OAI.SphericalPerceptronFreeEnergy.cavity_quadratic_log_integrable line 48
4. lemma OAI.SphericalPerceptronFreeEnergy.cavity_Q_ratio_integrable line 84
5. theorem OAI.SphericalPerceptronFreeEnergy.cavity_expected_log_drop_quadratic line 113
6. theorem OAI.SphericalPerceptronFreeEnergy.cavity_angular_expected_log_drop line 164
7. lemma OAI.SphericalPerceptronFreeEnergy.cavity_quadratic_cost_tendsto_zero line 192