OAI/Probability/SphericalField/Gibbs/GaussianIdentities.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptron.replicaMean_const line 19
2. lemma OAI.SphericalPerceptron.replicaMean_annealed_integrable line 26
3. lemma OAI.SphericalPerceptron.fieldCovariance_measurable line 39
4. lemma OAI.SphericalPerceptron.fieldCovariance_comp_measurable line 45
5. lemma OAI.SphericalPerceptron.fieldCovariance_bound line 52
6. lemma OAI.SphericalPerceptron.gaussian_field_energy_mean line 61
7. lemma OAI.SphericalPerceptron.gaussian_gg_defect_bound line 106