OAI/Probability/Perceptron/Pressure/HeightPartition.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptronFreeEnergy.heightIndex line 11
2. lemma OAI.SphericalPerceptronFreeEnergy.heightIndex_monotone line 17
3. lemma OAI.SphericalPerceptronFreeEnergy.heightIndex_le_iff line 25
4. lemma OAI.SphericalPerceptronFreeEnergy.lt_heightIndex_iff line 49
5. def OAI.SphericalPerceptronFreeEnergy.heightVariances line 53
6. lemma OAI.SphericalPerceptronFreeEnergy.heightVariances_nonneg line 56
7. lemma OAI.SphericalPerceptronFreeEnergy.heightVariances_sum line 60
8. lemma OAI.SphericalPerceptronFreeEnergy.heightVariances_prefix line 64
9. lemma OAI.SphericalPerceptronFreeEnergy.heightIndex_grid_prefix line 85