OAI/Probability/SphericalField/Poisson/Superposition.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptron.poissonRandomMeasureLaw_superposition line 18
2. lemma OAI.SphericalPerceptron.poissonRandomMeasureLaw_of_finite line 40
3. lemma OAI.SphericalPerceptron.aemeasurable_randomMeasure_lintegral_of_finite line 64
4. lemma OAI.SphericalPerceptron.poissonRandomMeasureLaw_ae_restrict_finite line 87
5. lemma OAI.SphericalPerceptron.poissonRandomMeasureLaw_ae_null line 97
6. lemma OAI.SphericalPerceptron.stablePoissonTotal_rpow_integrable line 107
7. lemma OAI.SphericalPerceptron.log_sq_le_two_rpow line 115
8. lemma OAI.SphericalPerceptron.stablePoissonTotal_weighted_log_sq_integrable line 136
9. lemma OAI.SphericalPerceptron.stablePoissonTotal_log_memLp_two line 159
10. lemma OAI.SphericalPerceptron.quadratic_contact_remainders line 169
11. lemma OAI.SphericalPerceptron.integral_convex_contact_bound line 180
12. lemma OAI.SphericalPerceptron.integral_centered_abs_le_sqrt_variance line 218
13. lemma OAI.SphericalPerceptron.measurable_measure_restrict line 233