OAI/Probability/SphericalField/Sphere/FiniteUniform.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptron.finiteAmplitudeSphereValue_uniform line 14
2. def OAI.SphericalPerceptron.fieldAmplitudes line 21
3. lemma OAI.SphericalPerceptron.fieldAmplitudes_last line 24
4. lemma OAI.SphericalPerceptron.fieldAmplitudes_increment line 28
5. lemma OAI.SphericalPerceptron.fieldAmplitudes_continuous line 35
6. lemma OAI.SphericalPerceptron.amplitudeCovarianceLevels_fieldAmplitudes line 44
7. lemma OAI.SphericalPerceptron.finiteAmplitudeSphereDual_fieldAmplitudes line 60
8. lemma OAI.SphericalPerceptron.finiteAmplitudeSphereValue_fieldAmplitudes line 67
9. theorem OAI.SphericalPerceptron.finiteSphericalFieldValue_compact_uniform line 79