OAI/Probability/Perceptron/Variational/Shape.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.countedBlockProbability_eq_excluded line 14
2. lemma OAI.SphericalPerceptronFreeEnergy.countedBlockProbability_embeddings line 28
3. lemma OAI.SphericalPerceptronFreeEnergy.indexedShapeRoot_embeddings line 40
4. def OAI.SphericalPerceptronFreeEnergy.trivialDecoratedShape line 67
5. lemma OAI.SphericalPerceptronFreeEnergy.trivialDecoratedShape_bare line 71
6. lemma OAI.SphericalPerceptronFreeEnergy.trivialDecoratedShape_valid line 80
7. lemma OAI.SphericalPerceptronFreeEnergy.trivialDecoratedShape_markValue line 94
8. lemma OAI.SphericalPerceptronFreeEnergy.trivialDecoratedShape_probability_succ line 112
9. lemma OAI.SphericalPerceptronFreeEnergy.indexedShapeVisit_eq_shape line 141
10. theorem OAI.SphericalPerceptronFreeEnergy.indexedShapeVisit_integral line 196