OAI/Probability/SphericalField/Gaussian/ExponentialNorm.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SphericalPerceptron.gaussian_integrable_exp_normline 17 - lemma
OAI.SphericalPerceptron.gaussian_integrable_norm_sq_expline 29 - lemma
OAI.SphericalPerceptron.gaussian_integrable_exp_lipschitzline 37 - lemma
OAI.SphericalPerceptron.gaussian_integrable_lipschitzline 56