OAI/Probability/Perceptron/Variational/ConvexUniform.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.equicontinuous_of_convex_nonneg_tendsto line 11
2. lemma OAI.SphericalPerceptronFreeEnergy.tendstoUniformlyOn_of_convex_nonneg_tendsto line 47
3. lemma OAI.SphericalPerceptronFreeEnergy.finiteAmplitudeSphereValue_uniform line 67
4. def OAI.SphericalPerceptronFreeEnergy.fieldAmplitudes line 74
5. lemma OAI.SphericalPerceptronFreeEnergy.fieldAmplitudes_last line 77
6. lemma OAI.SphericalPerceptronFreeEnergy.fieldAmplitudes_increment line 81
7. lemma OAI.SphericalPerceptronFreeEnergy.fieldAmplitudes_continuous line 88
8. lemma OAI.SphericalPerceptronFreeEnergy.amplitudeCovarianceLevels_fieldAmplitudes line 98
9. lemma OAI.SphericalPerceptronFreeEnergy.finiteAmplitudeSphereDual_fieldAmplitudes line 114
10. lemma OAI.SphericalPerceptronFreeEnergy.finiteAmplitudeSphereValue_fieldAmplitudes line 121
11. theorem OAI.SphericalPerceptronFreeEnergy.finiteSphericalFieldValue_compact_uniform line 133