OAI/Probability/SphericalField/Gibbs/ReplicaIdentity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptron.gibbsReplicaMean line 19
2. def OAI.SphericalPerceptron.fieldCovariance line 22
3. lemma OAI.SphericalPerceptron.replicaMean_measurable line 25
4. lemma OAI.SphericalPerceptron.replicaMean_bound line 33
5. lemma OAI.SphericalPerceptron.replicaMean_sum line 39
6. lemma OAI.SphericalPerceptron.replicaMean_const_mul line 49
7. lemma OAI.SphericalPerceptron.gaussian_replica_field_ibp line 53