OAI/Probability/SphericalField/Sphere/RadialBands.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptron.canonicalRadial_band_mass_bounds line 25
2. lemma OAI.SphericalPerceptron.canonicalRadial_band_log_bounds line 65
3. lemma OAI.SphericalPerceptron.canonicalRadial_band_log_eventually line 87
4. lemma OAI.SphericalPerceptron.unitSphere_continuous_integrable line 95
5. def OAI.SphericalPerceptron.sphericalExp line 101
6. lemma OAI.SphericalPerceptron.sphericalExp_even line 104
7. lemma OAI.SphericalPerceptron.sphericalExp_eq_cosh line 117
8. lemma OAI.SphericalPerceptron.sphericalExp_mono line 129
9. lemma OAI.SphericalPerceptron.one_le_sphericalExp line 139