OAI/Probability/Perceptron/Cascade/IndexedVertices.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SphericalPerceptronFreeEnergy.IndexedVertexline 11 - instance
OAI.SphericalPerceptronFreeEnergy.indexedVertex_countableline 15 - def
OAI.SphericalPerceptronFreeEnergy.indexedMarksFromVerticesline 20 - lemma
OAI.SphericalPerceptronFreeEnergy.indexedMarksFromVertices_measurableline 26 - lemma
OAI.SphericalPerceptronFreeEnergy.infinitePi_sumPiEquivProdPiline 38 - lemma
OAI.SphericalPerceptronFreeEnergy.indexedMarksFromVertices_lawline 47 - def
OAI.SphericalPerceptronFreeEnergy.indexedLeafVertexline 88 - lemma
OAI.SphericalPerceptronFreeEnergy.indexedLeafVertex_injectiveline 93