OAI/Probability/SphericalField/Sphere/Limit.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptron.normalizedCoordinateSphereLog_measurable line 13
2. lemma OAI.SphericalPerceptron.normalizedCoordinateSphereLog_integrable line 20
3. lemma OAI.SphericalPerceptron.normalizedCoordinateSphereLog_nonneg line 26
4. lemma OAI.SphericalPerceptron.expectedCoordinateSphereLog_upper line 35
5. lemma OAI.SphericalPerceptron.expectedCoordinateSphereLog_upper_eventually line 87
6. lemma OAI.SphericalPerceptron.normalizedCoordinateSphereLog_lower_probability line 103
7. lemma OAI.SphericalPerceptron.expectedCoordinateSphereLog_lower_eventually line 194
8. theorem OAI.SphericalPerceptron.expectedCoordinateSphereLog_tendsto line 209