OAI/Probability/Perceptron/Variational/EnrichedVarianceBound.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptronFreeEnergy.enrichedRandomPressure line 12
2. def OAI.SphericalPerceptronFreeEnergy.enrichedPoissonDisorderLaw line 16
3. instance OAI.SphericalPerceptronFreeEnergy.(instance at line 19) line 19
4. def OAI.SphericalPerceptronFreeEnergy.enrichedVarianceConstant line 24
5. lemma OAI.SphericalPerceptronFreeEnergy.enrichedRandomPressure_variance line 28
6. lemma OAI.SphericalPerceptronFreeEnergy.enrichedRandomPressure_centered_square line 79
7. def OAI.SphericalPerceptronFreeEnergy.sourceCascadeRealization line 92
8. lemma OAI.SphericalPerceptronFreeEnergy.sourceCascadeRealization_measurable line 97
9. lemma OAI.SphericalPerceptronFreeEnergy.sourceCascadeRealization_preserving line 104
10. abbrev OAI.SphericalPerceptronFreeEnergy.SourceIndexedDisorder line 123
11. def OAI.SphericalPerceptronFreeEnergy.sourceIndexedDisorderLaw line 126
12. instance OAI.SphericalPerceptronFreeEnergy.(instance at line 131) line 131
13. def OAI.SphericalPerceptronFreeEnergy.sourceDisorderRealization line 136
14. lemma OAI.SphericalPerceptronFreeEnergy.sourceDisorderRealization_preserving line 141
15. def OAI.SphericalPerceptronFreeEnergy.sourceIndexedPressure line 148
16. lemma OAI.SphericalPerceptronFreeEnergy.sourceIndexedPressure_memLp line 152
17. lemma OAI.SphericalPerceptronFreeEnergy.sourceIndexedPressure_variance line 160