OAI/Probability/SphericalField/Gibbs/Replicas.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptron.replica_partition line 19
2. lemma OAI.SphericalPerceptron.replica_mean_potential line 27
3. lemma OAI.SphericalPerceptron.gaussian_replica_integrationByParts line 48
4. lemma OAI.SphericalPerceptron.tilt_law_apply line 70
5. lemma OAI.SphericalPerceptron.tilt_law_pi line 81
6. lemma OAI.SphericalPerceptron.tilt_mean_twice line 102
7. lemma OAI.SphericalPerceptron.gaussian_pi_coordinate_integrationByParts line 119