OAI/Probability/Perceptron/Cavity/BulkRadialIBP.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptronFreeEnergy.freshRadial line 12
2. def OAI.SphericalPerceptronFreeEnergy.freshSecond line 14
3. def OAI.SphericalPerceptronFreeEnergy.freshRadialPair line 16
4. lemma OAI.SphericalPerceptronFreeEnergy.freshRadial_measurable line 19
5. lemma OAI.SphericalPerceptronFreeEnergy.freshSecond_measurable line 22
6. lemma OAI.SphericalPerceptronFreeEnergy.freshRadialPair_measurable line 25
7. lemma OAI.SphericalPerceptronFreeEnergy.freshRadial_bound line 29
8. lemma OAI.SphericalPerceptronFreeEnergy.freshSecond_bound line 34
9. lemma OAI.SphericalPerceptronFreeEnergy.freshRadialPair_bound line 40
10. lemma OAI.SphericalPerceptronFreeEnergy.fresh_radial_ibp line 49
11. lemma OAI.SphericalPerceptronFreeEnergy.bulk_radial_last_ibp line 74
12. lemma OAI.SphericalPerceptronFreeEnergy.bulk_radial_row_ibp line 105