OAI/Probability/Perceptron/Cavity/BulkThermal.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.bulkMarkNorm_memLp line 11
2. def OAI.SphericalPerceptronFreeEnergy.bulkThermalVar line 16
3. lemma OAI.SphericalPerceptronFreeEnergy.bulkThermalVar_measurable line 22
4. lemma OAI.SphericalPerceptronFreeEnergy.bulkThermalVar_nonneg line 28
5. lemma OAI.SphericalPerceptronFreeEnergy.bulkThermalVar_bound line 40
6. lemma OAI.SphericalPerceptronFreeEnergy.bulkThermalVar_integrable line 53
7. lemma OAI.SphericalPerceptronFreeEnergy.bulkExpectedSlope_hasDerivAt line 60
8. lemma OAI.SphericalPerceptronFreeEnergy.bulk_expected_slope_bound line 86
9. lemma OAI.SphericalPerceptronFreeEnergy.bulkExpectedThermalVar_measurable line 107
10. lemma OAI.SphericalPerceptronFreeEnergy.bulkExpectedThermalVar_intervalIntegrable line 116
11. lemma OAI.SphericalPerceptronFreeEnergy.bulkThermalVar_integrated_bound line 130