OAI/Probability/Perceptron/Cavity/CavityQuadraticDrop.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.cavity_log_drop_quadratic line 12
2. lemma OAI.SphericalPerceptronFreeEnergy.cavity_exp_abs_cauchy line 40
3. lemma OAI.SphericalPerceptronFreeEnergy.cavityLinearField_exp_integrable line 51
4. lemma OAI.SphericalPerceptronFreeEnergy.cavityLinearField_exp_memLp line 59
5. lemma OAI.SphericalPerceptronFreeEnergy.cavity_tilted_Q_conditional line 74
6. lemma OAI.SphericalPerceptronFreeEnergy.cavity_tilted_Q_uniform line 89
7. lemma OAI.SphericalPerceptronFreeEnergy.cavity_tilted_Q_integrable line 120
8. lemma OAI.SphericalPerceptronFreeEnergy.cavityLinearField_measurable line 128
9. lemma OAI.SphericalPerceptronFreeEnergy.cavityQuadraticField_measurable line 136
10. lemma OAI.SphericalPerceptronFreeEnergy.cavity_Q_product_integrable line 144
11. lemma OAI.SphericalPerceptronFreeEnergy.cavity_Q_normalized_bound line 181