OAI/Probability/SphericalField/Quantiles/Convergence.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptron.BoundedField.round_tendsto line 15
2. lemma OAI.SphericalPerceptron.quantileTail_tendsto line 22
3. lemma OAI.SphericalPerceptron.quantileA_tendsto_fixed line 38
4. lemma OAI.SphericalPerceptron.quantileA_tendsto_moving line 58
5. lemma OAI.SphericalPerceptron.BoundedField.stationary_tendsto line 74
6. lemma OAI.SphericalPerceptron.BoundedField.L1_tendsto line 79
7. lemma OAI.SphericalPerceptron.boundedSphericalFieldValue_tendsto_L1 line 94
8. lemma OAI.SphericalPerceptron.entropy_quantileTrial_tendsto line 101
9. lemma OAI.SphericalPerceptron.BoundedField.integral_mul_tendsto line 127