OAI/Probability/Perceptron/Cavity/CavityShellRestriction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.unitSphere_cavityAmbient_law line 13
2. lemma OAI.SphericalPerceptronFreeEnergy.cavityShellProbability_integral line 26
3. theorem OAI.SphericalPerceptronFreeEnergy.cavity_actual_shell_restriction line 35
4. lemma OAI.SphericalPerceptronFreeEnergy.cavityShell_bulkHamiltonian line 92
5. lemma OAI.SphericalPerceptronFreeEnergy.cavity_restriction_log_of_bounded line 100
6. lemma OAI.SphericalPerceptronFreeEnergy.cavity_actual_shell_log_restriction line 123
7. lemma OAI.SphericalPerceptronFreeEnergy.cavity_gaussian_log_integrable line 140