OAI/Probability/Perceptron/Sphere/SphereIsometryMap.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.sphereIsometryMap line 18
  2. lemma OAI.SphericalPerceptronFreeEnergy.sphereIsometryMap_measurable line 22
  3. lemma OAI.SphericalPerceptronFreeEnergy.sphereIsometryMap_preimage_cone line 26
  4. lemma OAI.SphericalPerceptronFreeEnergy.sphereIsometryMap_preserving line 39
  5. lemma OAI.SphericalPerceptronFreeEnergy.unitSphereLaw_isometry_preserving line 52
  6. lemma OAI.SphericalPerceptronFreeEnergy.sphereLaw_isometry_preserving line 59
  7. def OAI.SphericalPerceptronFreeEnergy.skewFlow line 77
  8. lemma OAI.SphericalPerceptronFreeEnergy.skewFlow_apply line 84
  9. lemma OAI.SphericalPerceptronFreeEnergy.skewFlow_zero line 87
  10. lemma OAI.SphericalPerceptronFreeEnergy.skewFlow_deriv line 90
  11. lemma OAI.SphericalPerceptronFreeEnergy.integrable_of_continuous_sphere_support line 97
  12. lemma OAI.SphericalPerceptronFreeEnergy.invariant_skew_integral_zero line 103
  13. def OAI.SphericalPerceptronFreeEnergy.planeSkew line 136
  14. lemma OAI.SphericalPerceptronFreeEnergy.planeSkew_mem line 140
  15. lemma OAI.SphericalPerceptronFreeEnergy.planeSkew_apply line 146
  16. lemma OAI.SphericalPerceptronFreeEnergy.rotation_product_deriv line 150
  17. lemma OAI.SphericalPerceptronFreeEnergy.sum_planeSkew line 161
  18. lemma OAI.SphericalPerceptronFreeEnergy.sum_planeSkew_divergence line 179
  19. lemma OAI.SphericalPerceptronFreeEnergy.invariant_tangent_integral line 193
  20. lemma OAI.SphericalPerceptronFreeEnergy.sphereLaw_ae_norm line 230
  21. lemma OAI.SphericalPerceptronFreeEnergy.sphere_integrable_of_continuous line 242
  22. lemma OAI.SphericalPerceptronFreeEnergy.sphere_tangent_integral line 246
  23. def OAI.SphericalPerceptronFreeEnergy.sphereOverlap line 260
  24. lemma OAI.SphericalPerceptronFreeEnergy.sphere_tangent_integral_normalized line 262
  25. lemma OAI.SphericalPerceptronFreeEnergy.sphereOverlap_hasFDerivAt line 285
  26. lemma OAI.SphericalPerceptronFreeEnergy.sphereOverlap_tangent_deriv line 290
  27. lemma OAI.SphericalPerceptronFreeEnergy.sphere_gibbs_tangent_identity line 298
  28. def OAI.SphericalPerceptronFreeEnergy.poissonMarkMeasure line 322
  29. def OAI.SphericalPerceptronFreeEnergy.normalizedMeasure line 325
  30. lemma OAI.SphericalPerceptronFreeEnergy.measurable_measure_withDensity_fixed line 328
  31. lemma OAI.SphericalPerceptronFreeEnergy.poissonMarkMeasure_measurable line 334
  32. lemma OAI.SphericalPerceptronFreeEnergy.normalizedMeasure_measurable line 339
  33. lemma OAI.SphericalPerceptronFreeEnergy.normalizedMeasure_probability line 345
  34. lemma OAI.SphericalPerceptronFreeEnergy.normalizedMeasure_smul line 351
  35. lemma OAI.SphericalPerceptronFreeEnergy.map_withDensity_comp line 361
  36. lemma OAI.SphericalPerceptronFreeEnergy.poissonMarkMeasure_shift line 371
  37. lemma OAI.SphericalPerceptronFreeEnergy.poissonMarkMeasure_mass line 384
  38. lemma OAI.SphericalPerceptronFreeEnergy.poissonMarkMeasure_probability line 390
  39. lemma OAI.SphericalPerceptronFreeEnergy.stablePoisson_gibbs_measure_law line 415