OAI/Probability/Perceptron/Cavity/BulkPairLaw.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SphericalPerceptronFreeEnergy.BulkPairRange line 12
2. def OAI.SphericalPerceptronFreeEnergy.bulkFiniteReplicaLaw line 14
3. instance OAI.SphericalPerceptronFreeEnergy.bulkFiniteReplicaLaw_probability line 22
4. lemma OAI.SphericalPerceptronFreeEnergy.bulkFiniteReplicaLaw_integral line 29
5. def OAI.SphericalPerceptronFreeEnergy.bulkCompactPair line 43
6. lemma OAI.SphericalPerceptronFreeEnergy.bulkCompactPair_measurable line 49
7. def OAI.SphericalPerceptronFreeEnergy.bulkPairLaw line 58
8. lemma OAI.SphericalPerceptronFreeEnergy.bulkPairLaw_integral line 63
9. lemma OAI.SphericalPerceptronFreeEnergy.bulkPairLaw_overlap line 78
10. lemma OAI.SphericalPerceptronFreeEnergy.compact_pair_zero_variance line 99
11. def OAI.SphericalPerceptronFreeEnergy.compactPairMarginal line 121
12. lemma OAI.SphericalPerceptronFreeEnergy.compactPairMarginal_integral line 125
13. lemma OAI.SphericalPerceptronFreeEnergy.bulkPairLaw_limit_marginal line 131
14. theorem OAI.SphericalPerceptronFreeEnergy.bulkPairLaw_identification line 153