OAI/Probability/SphericalField/Entropy/Kernel.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SphericalPerceptron.weighted_kernel_homogeneous_eq_zero line 16
2. def OAI.SphericalPerceptron.sphereKernel line 60
3. def OAI.SphericalPerceptron.sphereTail line 62
4. lemma OAI.SphericalPerceptron.sphereKernel_nonneg line 65
5. lemma OAI.SphericalPerceptron.sphereKernel_le_weight line 73
6. lemma OAI.SphericalPerceptron.sphereTail_integrable line 83
7. lemma OAI.SphericalPerceptron.sphereKernel_integrable line 96
8. lemma OAI.SphericalPerceptron.sphereTail_lower line 105
9. lemma OAI.SphericalPerceptron.sphereKernel_row_bound line 114
10. theorem OAI.SphericalPerceptron.sphere_equation_unique line 126
11. lemma OAI.SphericalPerceptron.sphereTail_nonneg line 168
12. lemma OAI.SphericalPerceptron.sphereTail_upper line 172
13. theorem OAI.SphericalPerceptron.sphere_equation_support_bound line 180