OAI/Probability/Perceptron/Cavity/BulkStein.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.bulkOverlapPower_measurable line 14
2. lemma OAI.SphericalPerceptronFreeEnergy.bulkOverlapPower_bound line 18
3. lemma OAI.SphericalPerceptronFreeEnergy.bulk_fixed_patterns_ibp_raw line 23
4. lemma OAI.SphericalPerceptronFreeEnergy.bulk_fixed_integrand_eq line 41
5. lemma OAI.SphericalPerceptronFreeEnergy.bulk_replicaPower_integrable_fixed line 64
6. lemma OAI.SphericalPerceptronFreeEnergy.bulk_fixed_patterns_ibp line 77
7. lemma OAI.SphericalPerceptronFreeEnergy.bulk_meanY_measurable line 89
8. lemma OAI.SphericalPerceptronFreeEnergy.bulk_meanY_bound line 97
9. lemma OAI.SphericalPerceptronFreeEnergy.bulk_meanY_integrable line 106
10. lemma OAI.SphericalPerceptronFreeEnergy.bulk_replicaPower_integrable line 115
11. lemma OAI.SphericalPerceptronFreeEnergy.bulk_annealed_ibp line 126
12. lemma OAI.SphericalPerceptronFreeEnergy.bulk_expected_slope_eq line 140