OAI/Probability/SphericalField/Poisson/DistinctMoments.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptron.cascadeMeasurableSet_exists line 24
2. lemma OAI.SphericalPerceptron.measurable_fin_cons line 30
3. def OAI.SphericalPerceptron.stableDistinctMoment line 39
4. lemma OAI.SphericalPerceptron.stableDistinctMoment_measurable line 44
5. lemma OAI.SphericalPerceptron.stableDistinctMoment_add_dirac line 60
6. instance OAI.SphericalPerceptron.stableLogIntensity_noAtoms line 75
7. lemma OAI.SphericalPerceptron.stableDistinctMoment_palm_laplace line 79
8. lemma OAI.SphericalPerceptron.stableLaplaceProduct_shape line 141
9. lemma OAI.SphericalPerceptron.list_length_mul_le_sum line 166
10. lemma OAI.SphericalPerceptron.stableDistinctMoment_palm_mellin_mul line 176