OAI/Probability/SphericalField/Entropy/Distribution.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptron.realTail line 16
2. def OAI.SphericalPerceptron.realCDF line 19
3. lemma OAI.SphericalPerceptron.continuous_time_integrable line 21
4. lemma OAI.SphericalPerceptron.realTail_integrable line 25
5. lemma OAI.SphericalPerceptron.hasDerivWithinAt_max_right line 29
6. lemma OAI.SphericalPerceptron.realTail_right_derivative line 40
7. lemma OAI.SphericalPerceptron.abs_realTail_sub_le line 83
8. lemma OAI.SphericalPerceptron.realTail_continuous line 94
9. lemma OAI.SphericalPerceptron.realCDF_monotone line 102
10. lemma OAI.SphericalPerceptron.realCDF_integrable line 107
11. lemma OAI.SphericalPerceptron.integral_cdf_mul line 111
12. lemma OAI.SphericalPerceptron.realTail_lower line 152