OAI/Probability/Perceptron/Variational/FocusedSampleLaw.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptronFreeEnergy.indexedSampleFocused line 11
2. lemma OAI.SphericalPerceptronFreeEnergy.indexedSampleFocused_measurable line 19
3. lemma OAI.SphericalPerceptronFreeEnergy.indexedFocusedVisit_zero_eq_sample line 29
4. lemma OAI.SphericalPerceptronFreeEnergy.indexedSampleFocused_eq_measure line 38
5. theorem OAI.SphericalPerceptronFreeEnergy.indexedSampleFocused_integral line 57
6. def OAI.SphericalPerceptronFreeEnergy.cascadeFocusCount line 83
7. lemma OAI.SphericalPerceptronFreeEnergy.cascadeFocusCount_zero line 88
8. lemma OAI.SphericalPerceptronFreeEnergy.cascadeFocusCount_succ line 92
9. lemma OAI.SphericalPerceptronFreeEnergy.focusedShapeNumerator_eq_count line 114