OAI/Probability/SphericalField/Sphere/EntropicParameter.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptron.mem_interior_integrableExpSet_of_all line 17
2. lemma OAI.SphericalPerceptron.cgf_analytic_of_all line 24
3. lemma OAI.SphericalPerceptron.cgf_second_nonneg line 29
4. lemma OAI.SphericalPerceptron.cgf_deriv_monotone line 39
5. def OAI.SphericalPerceptron.entropicMean line 45
6. lemma OAI.SphericalPerceptron.entropicMean_eq_div line 48
7. lemma OAI.SphericalPerceptron.entropicMean_zero line 58
8. lemma OAI.SphericalPerceptron.entropicMean_monotone line 62
9. lemma OAI.SphericalPerceptron.entropicMean_param_bound line 73
10. lemma OAI.SphericalPerceptron.cgf_second_le_of_moments line 110