OAI/Probability/Perceptron/Sphere/SphereHeat.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptronFreeEnergy.logSphericalExp line 12
2. lemma OAI.SphericalPerceptronFreeEnergy.sphericalExp_le_mul line 15
3. lemma OAI.SphericalPerceptronFreeEnergy.logSphericalExp_lipschitz line 33
4. lemma OAI.SphericalPerceptronFreeEnergy.logSphericalExp_nonneg line 52
5. lemma OAI.SphericalPerceptronFreeEnergy.logSphericalExp_zero line 55
6. lemma OAI.SphericalPerceptronFreeEnergy.integral_exp_inner_stdGaussian line 58
7. lemma OAI.SphericalPerceptronFreeEnergy.sphericalExp_gaussian_average line 71
8. lemma OAI.SphericalPerceptronFreeEnergy.gaussianEntropic_logSphericalExp_one line 117