OAI/Probability/SphericalField/Sphere/Rotations.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptron.skewFlow line 22
  2. lemma OAI.SphericalPerceptron.skewFlow_apply line 29
  3. lemma OAI.SphericalPerceptron.skewFlow_zero line 32
  4. lemma OAI.SphericalPerceptron.skewFlow_deriv line 35
  5. lemma OAI.SphericalPerceptron.integrable_of_continuous_sphere_support line 42
  6. lemma OAI.SphericalPerceptron.invariant_skew_integral_zero line 48
  7. def OAI.SphericalPerceptron.planeSkew line 81
  8. lemma OAI.SphericalPerceptron.planeSkew_mem line 85
  9. lemma OAI.SphericalPerceptron.planeSkew_apply line 91
  10. lemma OAI.SphericalPerceptron.rotation_product_deriv line 95
  11. lemma OAI.SphericalPerceptron.sum_planeSkew line 106
  12. lemma OAI.SphericalPerceptron.sum_planeSkew_divergence line 124
  13. lemma OAI.SphericalPerceptron.invariant_tangent_integral line 138
  14. lemma OAI.SphericalPerceptron.sphereLaw_ae_norm line 175
  15. lemma OAI.SphericalPerceptron.sphere_integrable_of_continuous line 183
  16. lemma OAI.SphericalPerceptron.sphere_tangent_integral line 187
  17. def OAI.SphericalPerceptron.sphereOverlap line 201
  18. lemma OAI.SphericalPerceptron.sphere_tangent_integral_normalized line 203
  19. lemma OAI.SphericalPerceptron.sphereOverlap_hasFDerivAt line 226
  20. lemma OAI.SphericalPerceptron.sphereOverlap_tangent_deriv line 231
  21. lemma OAI.SphericalPerceptron.sphere_gibbs_tangent_identity line 239