OAI/Probability/SphericalField/Poisson/StableMoments.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptron.lintegral_comp_exp_all line 23
2. lemma OAI.SphericalPerceptron.stableLogIntensity_laplace_moment line 30
3. lemma OAI.SphericalPerceptron.one_sub_exp_neg_lintegral line 63
4. lemma OAI.SphericalPerceptron.lintegral_rpow_unit line 80
5. lemma OAI.SphericalPerceptron.stableLaplaceConstant_eq_gamma line 90
6. lemma OAI.SphericalPerceptron.stablePoissonTotal_add_dirac line 117
7. lemma OAI.SphericalPerceptron.stablePoissonTotal_laplace_lintegral line 124
8. lemma OAI.SphericalPerceptron.stablePoisson_palm_laplace line 140
9. lemma OAI.SphericalPerceptron.gamma_lintegral_rpow_scale line 171
10. def OAI.SphericalPerceptron.stableJumpMomentE line 179
11. lemma OAI.SphericalPerceptron.stableJumpMomentE_measurable line 182