OAI/Probability/SphericalField/Gaussian/Integration.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptron.gaussianRotation line 16
2. lemma OAI.SphericalPerceptron.gaussianRotation_apply line 22
3. lemma OAI.SphericalPerceptron.gaussianRotation_preserving line 26
4. lemma OAI.SphericalPerceptron.integral_sq_ge_sq_integral_div line 47
5. lemma OAI.SphericalPerceptron.gaussian_rotation_path_bound line 74
6. lemma OAI.SphericalPerceptron.standardGaussian_secondMoment line 97
7. lemma OAI.SphericalPerceptron.hasDerivAt_bounded_memLp line 102
8. lemma OAI.SphericalPerceptron.gaussian_rotation_derivative_square_mean line 120
9. lemma OAI.SphericalPerceptron.integral_independent_difference_square line 135