OAI/Probability/SphericalField/Sphere/AmplitudeLimit.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptron.expectedCoordinateSphereLog_stationary_covariance line 14
  2. def OAI.SphericalPerceptron.amplitudeCovarianceLevels line 65
  3. lemma OAI.SphericalPerceptron.amplitudeCovarianceLevels_root line 69
  4. lemma OAI.SphericalPerceptron.amplitudeCovarianceLevels_increment line 72
  5. lemma OAI.SphericalPerceptron.amplitudeCovarianceLevels_monotone line 79
  6. lemma OAI.SphericalPerceptron.amplitudeCovarianceLevels_nonneg line 86
  7. def OAI.SphericalPerceptron.amplitudeSphereDual line 91
  8. lemma OAI.SphericalPerceptron.amplitudeSphereValue_tendsto line 96
  9. def OAI.SphericalPerceptron.finiteAmplitudeIncrement line 116
  10. def OAI.SphericalPerceptron.finiteAmplitudeSphereValue line 119
  11. def OAI.SphericalPerceptron.finiteAmplitudeSphereDual line 122
  12. lemma OAI.SphericalPerceptron.finiteAmplitudeSphereValue_convex line 126
  13. lemma OAI.SphericalPerceptron.finiteAmplitudeSphereValue_nonneg line 144
  14. lemma OAI.SphericalPerceptron.finiteAmplitudeSphereValue_tendsto line 150