OAI/Probability/Perceptron/Cavity/CavityTrueShellQ.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.cavity_shell_norm_bound line 13
2. lemma OAI.SphericalPerceptronFreeEnergy.cavityShellProbability_linear_one_le line 18
3. lemma OAI.SphericalPerceptronFreeEnergy.cavity_true_shell_denominator line 35
4. theorem OAI.SphericalPerceptronFreeEnergy.cavity_true_shell_expected_drop line 89
5. lemma OAI.SphericalPerceptronFreeEnergy.cavity_exp_integrable_bound line 114
6. lemma OAI.SphericalPerceptronFreeEnergy.cavity_gibbs_log_factorization line 122
7. theorem OAI.SphericalPerceptronFreeEnergy.cavity_actual_bulk_log_factorization line 147