OAI/Probability/SphericalField/Poisson/Mecke.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptron.poissonMeasure_succ_mul line 16
2. lemma OAI.SphericalPerceptron.finitePoissonLaw_mecke line 29
3. def OAI.SphericalPerceptron.stableLaplaceConstant line 84
4. lemma OAI.SphericalPerceptron.one_sub_exp_neg_le_min line 87
5. lemma OAI.SphericalPerceptron.stableLaplaceConstant_finite line 93
6. lemma OAI.SphericalPerceptron.stableLaplaceConstant_positive line 100
7. lemma OAI.SphericalPerceptron.stableLaplaceExponent_scaling line 113
8. def OAI.SphericalPerceptron.stablePoissonTotal line 126
9. lemma OAI.SphericalPerceptron.stablePoissonTotal_measurable line 129
10. lemma OAI.SphericalPerceptron.stablePoissonTotal_pos line 132
11. lemma OAI.SphericalPerceptron.stablePoissonTotal_laplace line 137
12. lemma OAI.SphericalPerceptron.standardGaussian_integrationByParts line 158