OAI/Probability/SphericalField/Gaussian/Rotations.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptron.dual_rotation_norm line 21
2. def OAI.SphericalPerceptron.gaussianVectorRotation line 32
3. lemma OAI.SphericalPerceptron.gaussianVectorRotation_apply line 39
4. lemma OAI.SphericalPerceptron.gaussianVectorRotation_preserving line 43
5. lemma OAI.SphericalPerceptron.stdGaussian_dual_secondMoment line 80
6. lemma OAI.SphericalPerceptron.hasFDerivAt_bounded_gaussian_memLp line 88
7. lemma OAI.SphericalPerceptron.gaussian_vector_rotation_path_bound line 107
8. lemma OAI.SphericalPerceptron.gaussian_vector_rotation_derivative_square_mean line 131
9. lemma OAI.SphericalPerceptron.stdGaussian_poincare line 157
10. lemma OAI.SphericalPerceptron.stdGaussian_variance_le_of_fderiv_bound line 209