OAI/Probability/SphericalField/Gibbs/Thermal.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptron.affineLogRoot line 20
  2. lemma OAI.SphericalPerceptron.affineLogRoot_eq line 23
  3. lemma OAI.SphericalPerceptron.affineLogRoot_deriv line 40
  4. lemma OAI.SphericalPerceptron.affineMean_deriv line 50
  5. lemma OAI.SphericalPerceptron.tilt_log_partition_bound line 64
  6. lemma OAI.SphericalPerceptron.affinePotential_bound line 81
  7. lemma OAI.SphericalPerceptron.affineLogRoot_convex line 86
  8. def OAI.SphericalPerceptron.thermalVar line 102
  9. lemma OAI.SphericalPerceptron.thermalVar_nonneg line 106
  10. lemma OAI.SphericalPerceptron.thermalVar_bound line 116
  11. lemma OAI.SphericalPerceptron.measurable_affineLogRoot line 133
  12. lemma OAI.SphericalPerceptron.measurable_affineMean line 139
  13. lemma OAI.SphericalPerceptron.measurable_thermalVar line 144
  14. lemma OAI.SphericalPerceptron.annealedAffineLogRoot_deriv line 151
  15. lemma OAI.SphericalPerceptron.annealedAffineMean_deriv line 178
  16. lemma OAI.SphericalPerceptron.contact_thermal_variance_le line 205