OAI/Probability/SphericalField/Fields/HeightPartition.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptron.heightIndex line 13
2. lemma OAI.SphericalPerceptron.heightIndex_monotone line 19
3. lemma OAI.SphericalPerceptron.heightIndex_le_iff line 27
4. lemma OAI.SphericalPerceptron.lt_heightIndex_iff line 51
5. def OAI.SphericalPerceptron.heightVariances line 55
6. lemma OAI.SphericalPerceptron.heightVariances_nonneg line 58
7. lemma OAI.SphericalPerceptron.heightVariances_sum line 62
8. lemma OAI.SphericalPerceptron.heightVariances_prefix line 66
9. lemma OAI.SphericalPerceptron.heightIndex_grid_prefix line 87