OAI/Probability/SphericalField/Poisson/MarkMeasure.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptron.poissonMarkMeasure line 17
2. lemma OAI.SphericalPerceptron.poissonMarkMeasure_measurable line 20
3. lemma OAI.SphericalPerceptron.normalizedMeasure_probability line 25
4. lemma OAI.SphericalPerceptron.normalizedMeasure_smul line 31
5. lemma OAI.SphericalPerceptron.map_withDensity_comp line 41
6. lemma OAI.SphericalPerceptron.poissonMarkMeasure_shift line 51
7. lemma OAI.SphericalPerceptron.poissonMarkMeasure_mass line 64
8. lemma OAI.SphericalPerceptron.poissonMarkMeasure_probability line 70
9. lemma OAI.SphericalPerceptron.stablePoisson_gibbs_measure_law line 95
10. abbrev OAI.SphericalPerceptron.CovarianceMatrix line 116
11. instance OAI.SphericalPerceptron.covarianceMatrixMeasurableSpace line 118
12. instance OAI.SphericalPerceptron.covarianceMatrixBorelSpace line 122
13. def OAI.SphericalPerceptron.gaussianCovarianceLaw line 126
14. lemma OAI.SphericalPerceptron.gaussianCovarianceLaw_continuous line 129
15. lemma OAI.SphericalPerceptron.gaussianCovariance_integral_continuous line 154
16. lemma OAI.SphericalPerceptron.gaussianCovariance_integral_tendsto line 160