OAI/Probability/Perceptron/Variational/DecoratedShapeLaw.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.exponentialMarkTilt_eq_density_of_one line 15
2. theorem OAI.SphericalPerceptronFreeEnergy.decoratedShapeProbability_integral line 27
3. def OAI.SphericalPerceptronFreeEnergy.PairedVisitShape line 118
4. def OAI.SphericalPerceptronFreeEnergy.PairedVisitShape.first line 122
5. def OAI.SphericalPerceptronFreeEnergy.PairedVisitShape.second line 126
6. def OAI.SphericalPerceptronFreeEnergy.PairedVisitShape.product line 130
7. lemma OAI.SphericalPerceptronFreeEnergy.PairedVisitShape.bare_first_second line 134
8. lemma OAI.SphericalPerceptronFreeEnergy.PairedVisitShape.product_valid line 142
9. theorem OAI.SphericalPerceptronFreeEnergy.decoratedShapeMarkValue_product line 155