OAI/Probability/Perceptron/Cascade/IndexedVertices.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.IndexedVertex line 11
  2. instance OAI.SphericalPerceptronFreeEnergy.indexedVertex_countable line 15
  3. def OAI.SphericalPerceptronFreeEnergy.indexedMarksFromVertices line 20
  4. lemma OAI.SphericalPerceptronFreeEnergy.indexedMarksFromVertices_measurable line 26
  5. lemma OAI.SphericalPerceptronFreeEnergy.infinitePi_sumPiEquivProdPi line 38
  6. lemma OAI.SphericalPerceptronFreeEnergy.indexedMarksFromVertices_law line 47
  7. def OAI.SphericalPerceptronFreeEnergy.indexedLeafVertex line 88
  8. lemma OAI.SphericalPerceptronFreeEnergy.indexedLeafVertex_injective line 93