OAI/Probability/Perceptron/Interpolation/KernelInfiniteReplica.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.kernelFiniteProduct_measurable line 17
2. lemma OAI.SphericalPerceptronFreeEnergy.kernelInfiniteReplica_measurable line 24
3. def OAI.SphericalPerceptronFreeEnergy.kernelInfiniteReplica line 38
4. instance OAI.SphericalPerceptronFreeEnergy.(instance at line 41) line 41
5. lemma OAI.SphericalPerceptronFreeEnergy.infiniteReplica_prefix_preserving line 45
6. lemma OAI.SphericalPerceptronFreeEnergy.kernelInfiniteReplica_prefix_integral line 59
7. def OAI.SphericalPerceptronFreeEnergy.annealedInfiniteReplicaMeasure line 72
8. instance OAI.SphericalPerceptronFreeEnergy.(instance at line 76) line 76
9. lemma OAI.SphericalPerceptronFreeEnergy.annealedInfiniteReplica_prefix_integral line 81
10. lemma OAI.SphericalPerceptronFreeEnergy.annealedInfiniteReplica_gibbs_prefix line 96
11. def OAI.SphericalPerceptronFreeEnergy.sourceJointOverlap line 108
12. lemma OAI.SphericalPerceptronFreeEnergy.sourceJointOverlap_measurable line 116
13. def OAI.SphericalPerceptronFreeEnergy.sourceJointArray line 126
14. lemma OAI.SphericalPerceptronFreeEnergy.sourceJointArray_measurable line 129
15. def OAI.SphericalPerceptronFreeEnergy.sourceGibbsArrayLaw line 136
16. lemma OAI.SphericalPerceptronFreeEnergy.sourceGibbsArray_integral line 145
17. lemma OAI.SphericalPerceptronFreeEnergy.sourceGibbsArray_block_integral line 154