OAI/Probability/SphericalField/Fields/HeightWord.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptron.extendedFieldExponents line 13
2. def OAI.SphericalPerceptron.finiteFieldCDFLeft line 16
3. lemma OAI.SphericalPerceptron.extendedFieldExponents_castSucc line 19
4. lemma OAI.SphericalPerceptron.extendedFieldExponents_last line 32
5. lemma OAI.SphericalPerceptron.extendedFieldExponents_nonneg line 36
6. lemma OAI.SphericalPerceptron.extendedFieldExponents_heightIndex line 42
7. lemma OAI.SphericalPerceptron.sphericalHeatValue_compress line 46
8. lemma OAI.SphericalPerceptron.sphericalHeatValue_drop_last_one line 63
9. lemma OAI.SphericalPerceptron.finiteSphericalFieldValue_height_word line 77