OAI/Probability/Perceptron/Cavity/CavityGaussianReplica.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptronFreeEnergy.cavityTestReplica line 17
2. lemma OAI.SphericalPerceptronFreeEnergy.cavityTestReplica_apply line 22
3. theorem OAI.SphericalPerceptronFreeEnergy.cavity_marked_moment line 27
4. def OAI.SphericalPerceptronFreeEnergy.cavitySingleTest line 84
5. lemma OAI.SphericalPerceptronFreeEnergy.cavitySingleTest_apply line 90
6. lemma OAI.SphericalPerceptronFreeEnergy.cavitySingleTest_replica line 97
7. lemma OAI.SphericalPerceptronFreeEnergy.posSemidef_independent_blocks line 104
8. lemma OAI.SphericalPerceptronFreeEnergy.cavityBlockCovariance_posSemidef line 125
9. lemma OAI.SphericalPerceptronFreeEnergy.bulkMarkedEntry_B_posSemidef line 139
10. lemma OAI.SphericalPerceptronFreeEnergy.bulkMarkedEntry_R_posSemidef line 153
11. lemma OAI.SphericalPerceptronFreeEnergy.cavityArrayKernel_actual line 159