OAI/Probability/Perceptron/Variational/IntegratedConvex.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.convex_derivative_monotone line 12
  2. lemma OAI.SphericalPerceptronFreeEnergy.integral_convex_derivative_fluctuation line 18
  3. lemma OAI.SphericalPerceptronFreeEnergy.convex_integrated_derivative_shift line 53
  4. lemma OAI.SphericalPerceptronFreeEnergy.integrated_convex_fluctuation_bound line 78
  5. def OAI.SphericalPerceptronFreeEnergy.countableGaussianVector line 99
  6. lemma OAI.SphericalPerceptronFreeEnergy.countableGaussianVector_measurable line 102
  7. lemma OAI.SphericalPerceptronFreeEnergy.countableGaussianVector_law line 106
  8. lemma OAI.SphericalPerceptronFreeEnergy.countableGaussianVector_preserving line 116
  9. def OAI.SphericalPerceptronFreeEnergy.vectorGaussianRow line 120
  10. def OAI.SphericalPerceptronFreeEnergy.vectorGaussianLength line 123
  11. lemma OAI.SphericalPerceptronFreeEnergy.vectorGaussianRow_measurable line 126
  12. lemma OAI.SphericalPerceptronFreeEnergy.vectorGaussianRow_field line 136
  13. lemma OAI.SphericalPerceptronFreeEnergy.vectorGaussianRow_norm line 143
  14. lemma OAI.SphericalPerceptronFreeEnergy.vectorGaussianRow_covariance line 150
  15. lemma OAI.SphericalPerceptronFreeEnergy.euclideanGaussian_tiltMean_ibp line 167