OAI/Probability/Perceptron/Variational/LocalMaxSecondDerivNonpos.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.localMax_second_deriv_nonpos line 17
  2. lemma OAI.SphericalPerceptronFreeEnergy.quadratic_contact_second_deriv line 28
  3. def OAI.SphericalPerceptronFreeEnergy.affineLogRoot line 48
  4. lemma OAI.SphericalPerceptronFreeEnergy.affineLogRoot_eq line 51
  5. lemma OAI.SphericalPerceptronFreeEnergy.affineLogRoot_deriv line 68
  6. lemma OAI.SphericalPerceptronFreeEnergy.affineMean_deriv line 78
  7. lemma OAI.SphericalPerceptronFreeEnergy.tilt_log_partition_bound line 92
  8. lemma OAI.SphericalPerceptronFreeEnergy.affinePotential_bound line 109
  9. lemma OAI.SphericalPerceptronFreeEnergy.affineLogRoot_convex line 114
  10. def OAI.SphericalPerceptronFreeEnergy.thermalVar line 127
  11. lemma OAI.SphericalPerceptronFreeEnergy.thermalVar_nonneg line 131
  12. lemma OAI.SphericalPerceptronFreeEnergy.thermalVar_bound line 141
  13. lemma OAI.SphericalPerceptronFreeEnergy.measurable_affineLogRoot line 158
  14. lemma OAI.SphericalPerceptronFreeEnergy.measurable_affineMean line 164
  15. lemma OAI.SphericalPerceptronFreeEnergy.measurable_thermalVar line 169
  16. lemma OAI.SphericalPerceptronFreeEnergy.annealedAffineLogRoot_deriv line 176
  17. lemma OAI.SphericalPerceptronFreeEnergy.annealedAffineMean_deriv line 203
  18. lemma OAI.SphericalPerceptronFreeEnergy.contact_thermal_variance_le line 230