OAI/Probability/SphericalField/Sphere/Heat.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptron.logSphericalExp line 14
2. lemma OAI.SphericalPerceptron.sphericalExp_le_mul line 17
3. lemma OAI.SphericalPerceptron.logSphericalExp_lipschitz line 35
4. lemma OAI.SphericalPerceptron.logSphericalExp_nonneg line 54
5. lemma OAI.SphericalPerceptron.logSphericalExp_zero line 57
6. lemma OAI.SphericalPerceptron.integral_exp_inner_stdGaussian line 60
7. lemma OAI.SphericalPerceptron.sphericalExp_gaussian_average line 72
8. lemma OAI.SphericalPerceptron.gaussianEntropic_logSphericalExp_one line 118