OAI/Probability/SphericalField/Gibbs/Energy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptron.integral_observable_factorization_bound line 20
2. lemma OAI.SphericalPerceptron.replicaMean_energy_factorization_bound line 44
3. lemma OAI.SphericalPerceptron.measurable_tiltMean_param line 63
4. lemma OAI.SphericalPerceptron.measurable_replicaMean_param line 70
5. lemma OAI.SphericalPerceptron.annealed_replica_energy_factorization_bound line 79
6. lemma OAI.SphericalPerceptron.localMax_second_deriv_nonpos line 123
7. lemma OAI.SphericalPerceptron.quadratic_contact_second_deriv line 134