OAI/Probability/Perceptron/Cascade/EnrichedPoissonVariance.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptronFreeEnergy.infinitePatternRowsLaw line 13
2. instance OAI.SphericalPerceptronFreeEnergy.(instance at line 16) line 16
3. def OAI.SphericalPerceptronFreeEnergy.patternPrefix line 20
4. lemma OAI.SphericalPerceptronFreeEnergy.patternPrefix_measurable line 23
5. lemma OAI.SphericalPerceptronFreeEnergy.patternPrefix_measurePreserving line 27
6. lemma OAI.SphericalPerceptronFreeEnergy.normalizedPatternEnergy_prefix_succ line 35
7. def OAI.SphericalPerceptronFreeEnergy.enrichedPoissonLog line 44
8. def OAI.SphericalPerceptronFreeEnergy.enrichedRowsDisorderLaw line 50
9. instance OAI.SphericalPerceptronFreeEnergy.(instance at line 53) line 53
10. lemma OAI.SphericalPerceptronFreeEnergy.enrichedPoissonLog_measurable line 58
11. lemma OAI.SphericalPerceptronFreeEnergy.enrichedPoissonLog_section_variance line 69
12. lemma OAI.SphericalPerceptronFreeEnergy.enrichedPoissonLog_mean_succ line 91
13. lemma OAI.SphericalPerceptronFreeEnergy.enrichedPoissonLog_variance line 111