OAI/Probability/Perceptron/Cavity/CavityTrueShellLower.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.cavity_sphericalExp_bound line 11
2. lemma OAI.SphericalPerceptronFreeEnergy.cavity_shell_compensator_bound line 15
3. theorem OAI.SphericalPerceptronFreeEnergy.cavity_true_shell_linear_lower line 28
4. lemma OAI.SphericalPerceptronFreeEnergy.cavityVectorField_norm_le line 106
5. lemma OAI.SphericalPerceptronFreeEnergy.cavity_angular_partition line 118
6. lemma OAI.SphericalPerceptronFreeEnergy.cavity_angular_log_integrable line 145
7. theorem OAI.SphericalPerceptronFreeEnergy.cavity_expected_shell_lower line 165