OAI/Probability/SphericalField/Gaussian/Taylor.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptron.gaussian_abs_moment line 16
2. lemma OAI.SphericalPerceptron.gaussian_law_integrable_abs_pow line 28
3. lemma OAI.SphericalPerceptron.gaussian_law_sq_mean line 38
4. lemma OAI.SphericalPerceptron.bounded_real_integrable line 48
5. lemma OAI.SphericalPerceptron.boundedContinuousFunction_integrable_comp line 53
6. lemma OAI.SphericalPerceptron.gaussian_taylor_mean_bound line 59
7. lemma OAI.SphericalPerceptron.drift_shift_mean_bound line 126
8. lemma OAI.SphericalPerceptron.gaussian_drift_taylor_mean_bound line 176