OAI/Probability/SphericalField/Poisson/PositiveMass.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptron.poissonRandomMeasureLaw_lintegral_pos_of_infinite line 16
2. lemma OAI.SphericalPerceptron.stablePoisson_total_positive line 46
3. lemma OAI.SphericalPerceptron.standardGaussian_density_deriv line 52
4. lemma OAI.SphericalPerceptron.standardGaussian_density_mul_integrable line 63
5. def OAI.SphericalPerceptron.finiteMeasureCutKernel line 73
6. instance OAI.SphericalPerceptron.finiteMeasureCutKernel_finite line 78
7. lemma OAI.SphericalPerceptron.aemeasurable_measure_lintegral_of_finite line 86
8. lemma OAI.SphericalPerceptron.finitePoissonLaw_ae_finite line 106
9. lemma OAI.SphericalPerceptron.finitePointMeasure_insertNth line 116
10. lemma OAI.SphericalPerceptron.finite_point_mecke line 123