OAI/Probability/SphericalField/Quantiles/AlmostEverywhere.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptron.quantileTrial_congr line 14
2. lemma OAI.SphericalPerceptron.quantileTail_congr line 24
3. lemma OAI.SphericalPerceptron.quantileA_congr line 27
4. lemma OAI.SphericalPerceptron.clippedQuantile_ae_eq line 32
5. lemma OAI.SphericalPerceptron.stationaryQuantileField_ae_eq line 39
6. lemma OAI.SphericalPerceptron.stationaryQuantileField_cross line 47
7. lemma OAI.SphericalPerceptron.entropy_quantileTrial_finite_of_ae_bounded line 57