OAI/Probability/SphericalField/Gibbs/Contact.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptron.tilt_mean_centered_abs_sq_le line 20
2. lemma OAI.SphericalPerceptron.tiltMean_nonneg line 38
3. lemma OAI.SphericalPerceptron.annealed_thermal_abs_sq_le line 44
4. lemma OAI.SphericalPerceptron.affineLogRoot_memLp line 94
5. lemma OAI.SphericalPerceptron.tilt_mean_center_triangle line 108
6. lemma OAI.SphericalPerceptron.contact_energy_L1_bound line 127