OAI/Probability/Perceptron/Sphere/GaussianPolar.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.canonicalRadial_exp_integrable line 12
2. lemma OAI.SphericalPerceptronFreeEnergy.canonicalRadial_exp_integral line 19
3. lemma OAI.SphericalPerceptronFreeEnergy.canonicalRadialMass_eq_stdGaussian line 27
4. def OAI.SphericalPerceptronFreeEnergy.gaussianRadialWeight line 49
5. def OAI.SphericalPerceptronFreeEnergy.gaussianRadiusLaw line 52
6. lemma OAI.SphericalPerceptronFreeEnergy.stdGaussian_polar_lintegral line 56
7. instance OAI.SphericalPerceptronFreeEnergy.gaussianRadiusLaw_probability line 69
8. lemma OAI.SphericalPerceptronFreeEnergy.normalizedGaussian_smul line 74
9. lemma OAI.SphericalPerceptronFreeEnergy.normalizedGaussian_polar_law line 81