OAI/Probability/Perceptron/Variational/DiagonalDeviation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.exists_slow_diagonal line 11
2. def OAI.SphericalPerceptronFreeEnergy.diagonalDeviationMass line 43
3. def OAI.SphericalPerceptronFreeEnergy.diagonalDeviationThreshold line 46
4. def OAI.SphericalPerceptronFreeEnergy.diagonalGoodSet line 49
5. lemma OAI.SphericalPerceptronFreeEnergy.diagonalDeviationThreshold_pos line 52
6. lemma OAI.SphericalPerceptronFreeEnergy.diagonalGoodSet_measurable line 57
7. lemma OAI.SphericalPerceptronFreeEnergy.diagonalGoodSet_compl_bound line 63
8. lemma OAI.SphericalPerceptronFreeEnergy.diagonalGoodSet_compl_tendsto line 90
9. lemma OAI.SphericalPerceptronFreeEnergy.diagonalDeviationThreshold_tendsto line 98
10. lemma OAI.SphericalPerceptronFreeEnergy.diagonalGoodSet_deviation_tendsto line 109