OAI/Probability/Perceptron/Cavity/CavityTelescoping.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.block_increment_linear_lower line 13
2. lemma OAI.SphericalPerceptronFreeEnergy.block_increment_asymptotic_lower line 41
3. lemma OAI.SphericalPerceptronFreeEnergy.cavity_averaged_log_lower line 56
4. lemma OAI.SphericalPerceptronFreeEnergy.normalizedPatternLog_integrable line 91
5. lemma OAI.SphericalPerceptronFreeEnergy.bulkExpectedLog_unperturbed_bound line 101
6. lemma OAI.SphericalPerceptronFreeEnergy.cavityAveragedLog_unperturbed_bound line 141
7. lemma OAI.SphericalPerceptronFreeEnergy.bulkScale_per_coordinate_tendsto line 169