OAI/Probability/Perceptron/Sphere/GaussianRotation.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.charFunDual_standardGaussian line 14
  2. def OAI.SphericalPerceptronFreeEnergy.gaussianRotation line 32
  3. lemma OAI.SphericalPerceptronFreeEnergy.gaussianRotation_apply line 38
  4. lemma OAI.SphericalPerceptronFreeEnergy.gaussianRotation_preserving line 42
  5. lemma OAI.SphericalPerceptronFreeEnergy.integral_sq_ge_sq_integral_div line 63
  6. lemma OAI.SphericalPerceptronFreeEnergy.gaussian_rotation_path_bound line 90
  7. lemma OAI.SphericalPerceptronFreeEnergy.standardGaussian_secondMoment line 113
  8. lemma OAI.SphericalPerceptronFreeEnergy.hasDerivAt_bounded_memLp line 118
  9. lemma OAI.SphericalPerceptronFreeEnergy.gaussian_rotation_derivative_square_mean line 136
  10. lemma OAI.SphericalPerceptronFreeEnergy.integral_independent_difference_square line 151
  11. lemma OAI.SphericalPerceptronFreeEnergy.standardGaussian_poincare line 170
  12. lemma OAI.SphericalPerceptronFreeEnergy.dual_rotation_norm line 226
  13. def OAI.SphericalPerceptronFreeEnergy.gaussianVectorRotation line 237
  14. lemma OAI.SphericalPerceptronFreeEnergy.gaussianVectorRotation_apply line 244
  15. lemma OAI.SphericalPerceptronFreeEnergy.gaussianVectorRotation_preserving line 248
  16. lemma OAI.SphericalPerceptronFreeEnergy.stdGaussian_dual_secondMoment line 285
  17. lemma OAI.SphericalPerceptronFreeEnergy.hasFDerivAt_bounded_gaussian_memLp line 293
  18. lemma OAI.SphericalPerceptronFreeEnergy.gaussian_vector_rotation_path_bound line 312
  19. lemma OAI.SphericalPerceptronFreeEnergy.gaussian_vector_rotation_derivative_square_mean line 336
  20. lemma OAI.SphericalPerceptronFreeEnergy.stdGaussian_poincare line 362
  21. lemma OAI.SphericalPerceptronFreeEnergy.stdGaussian_variance_le_of_fderiv_bound line 414