OAI/Probability/SphericalField/Gibbs/ReplicaCalculus.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptron.tilt_replica_integral line 19
2. lemma OAI.SphericalPerceptron.tilt_replica_coordinate line 28
3. lemma OAI.SphericalPerceptron.tilt_mean_sum line 37
4. lemma OAI.SphericalPerceptron.tilt_replica_sum line 47
5. lemma OAI.SphericalPerceptron.tilt_replica_new_product line 61
6. lemma OAI.SphericalPerceptron.gaussianField_replica line 90
7. lemma OAI.SphericalPerceptron.replicaPotential_add_field line 98
8. lemma OAI.SphericalPerceptron.gaussian_replica_coordinate_ibp line 113
9. lemma OAI.SphericalPerceptron.gamma_lintegral_positive_scale line 161
10. lemma OAI.SphericalPerceptron.integrable_rpow_neg_of_laplace line 183
11. lemma OAI.SphericalPerceptron.stablePoissonTotal_negative_integrable line 229