OAI/Probability/Perceptron/Variational/CompactGGFiniteCode.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptronFreeEnergy.compactCodeArray line 15
2. def OAI.SphericalPerceptronFreeEnergy.compactCodeBlock line 18
3. lemma OAI.SphericalPerceptronFreeEnergy.compactCodeArray_measurable line 21
4. lemma OAI.SphericalPerceptronFreeEnergy.compactCodeBlock_measurable line 28
5. lemma OAI.SphericalPerceptronFreeEnergy.compactGG_finite_pushforward line 35
6. lemma OAI.SphericalPerceptronFreeEnergy.compact_finite_code_block_unique line 57
7. def OAI.SphericalPerceptronFreeEnergy.scaledStdGaussian line 115
8. instance OAI.SphericalPerceptronFreeEnergy.(instance at line 117) line 117
9. lemma OAI.SphericalPerceptronFreeEnergy.scaledStdGaussian_conv line 120
10. lemma OAI.SphericalPerceptronFreeEnergy.stdGaussian_integral_add line 135
11. lemma OAI.SphericalPerceptronFreeEnergy.gaussianEntropic_semigroup line 156
12. lemma OAI.SphericalPerceptronFreeEnergy.gaussianEntropic_variance_zero line 181