OAI/Probability/SphericalField/Gaussian/Fractional.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptron.standardGaussian_quadratic_integral line 17
  2. lemma OAI.SphericalPerceptron.gaussian_quadratic_fractional_integrable line 30
  3. lemma OAI.SphericalPerceptron.gaussian_quadratic_fractional_log line 42
  4. lemma OAI.SphericalPerceptron.gaussianShiftStep_measurable line 63
  5. def OAI.SphericalPerceptron.quadraticCascadePrecision line 67
  6. def OAI.SphericalPerceptron.quadraticCascadeOffset line 71
  7. lemma OAI.SphericalPerceptron.quadraticCascadePrecision_tail_pos line 77
  8. theorem OAI.SphericalPerceptron.finiteCascade_quadratic_recursion line 84
  9. theorem OAI.SphericalPerceptron.canonical_cascade_quadratic_log line 115
  10. lemma OAI.SphericalPerceptron.canonical_scalar_integrable line 127
  11. lemma OAI.SphericalPerceptron.canonical_scalar_integral line 134
  12. lemma OAI.SphericalPerceptron.canonical_scalar_log line 142
  13. lemma OAI.SphericalPerceptron.quadraticCascadePrecision_le line 149
  14. lemma OAI.SphericalPerceptron.quadraticCascadePrecision_hasDerivAt line 159
  15. def OAI.SphericalPerceptron.quadraticCascadeReciprocalSlope line 165
  16. lemma OAI.SphericalPerceptron.quadraticCascadeOffset_hasDerivAt line 171
  17. def OAI.SphericalPerceptron.canonicalGaussianFreeValue line 183
  18. lemma OAI.SphericalPerceptron.canonicalGaussianFreeValue_hasDerivAt line 186