OAI/Probability/Perceptron/Variational/IndexedGaussianMarks.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.countableCoordinate line 13
  2. lemma OAI.SphericalPerceptronFreeEnergy.countableCoordinate_injective line 16
  3. def OAI.SphericalPerceptronFreeEnergy.countableGaussianVectors line 24
  4. lemma OAI.SphericalPerceptronFreeEnergy.countableGaussianVectors_measurable line 27
  5. lemma OAI.SphericalPerceptronFreeEnergy.countableGaussianVectors_law line 33
  6. abbrev OAI.SphericalPerceptronFreeEnergy.SharedVertex line 52
  7. def OAI.SphericalPerceptronFreeEnergy.indexedGaussianDisorder line 54
  8. lemma OAI.SphericalPerceptronFreeEnergy.indexedGaussianDisorder_measurable line 59
  9. lemma OAI.SphericalPerceptronFreeEnergy.indexedGaussianDisorder_law line 66
  10. lemma OAI.SphericalPerceptronFreeEnergy.indexedLeafState_gaussianLinear line 86
  11. def OAI.SphericalPerceptronFreeEnergy.indexedLeafSharedVertex line 111
  12. lemma OAI.SphericalPerceptronFreeEnergy.indexedLeafSharedVertex_injective line 114