OAI/Probability/Perceptron/Cavity/CavityIncrementLaw.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SphericalPerceptronFreeEnergy.CavityIncrementRandom line 13
2. def OAI.SphericalPerceptronFreeEnergy.cavityIncrementLaw line 16
3. instance OAI.SphericalPerceptronFreeEnergy.(instance at line 20) line 20
4. def OAI.SphericalPerceptronFreeEnergy.cavityIncrementFullRows line 24
5. lemma OAI.SphericalPerceptronFreeEnergy.cavityIncrementFullRows_preserving line 29
6. lemma OAI.SphericalPerceptronFreeEnergy.cavityShellLowLog_measurable line 59
7. lemma OAI.SphericalPerceptronFreeEnergy.cavityIncrement_actual_integrable line 72
8. lemma OAI.SphericalPerceptronFreeEnergy.cavityIncrement_actual_expectation line 81
9. lemma OAI.SphericalPerceptronFreeEnergy.finiteRows_toLp_preserving line 91
10. lemma OAI.SphericalPerceptronFreeEnergy.cavityFreshMajorant_rows_integrable line 98
11. lemma OAI.SphericalPerceptronFreeEnergy.cavityFreshMajorant_rows_mean_bound line 106
12. abbrev OAI.SphericalPerceptronFreeEnergy.CavityProxyRandom line 118
13. def OAI.SphericalPerceptronFreeEnergy.cavityProxyLaw line 119
14. instance OAI.SphericalPerceptronFreeEnergy.(instance at line 121) line 121
15. def OAI.SphericalPerceptronFreeEnergy.cavityProxyProjection line 124
16. lemma OAI.SphericalPerceptronFreeEnergy.cavityProxyProjection_preserving line 126
17. def OAI.SphericalPerceptronFreeEnergy.cavityProxyHamiltonian line 130
18. def OAI.SphericalPerceptronFreeEnergy.cavityProxyLog line 134
19. lemma OAI.SphericalPerceptronFreeEnergy.cavityProxyHamiltonian_measurable line 137
20. lemma OAI.SphericalPerceptronFreeEnergy.cavityProxyLog_measurable line 161
21. lemma OAI.SphericalPerceptronFreeEnergy.cavityProxyHamiltonian_bound line 167
22. lemma OAI.SphericalPerceptronFreeEnergy.cavityProxyLog_integrable line 176
23. lemma OAI.SphericalPerceptronFreeEnergy.cavityProxyLog_section_integrable line 198