OAI/Probability/SphericalField/Positivity/JointLaw.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptron.measurableSet_gram_arrays line 16
2. lemma OAI.SphericalPerceptron.scalarArray_ultrametric line 35
3. def OAI.SphericalPerceptron.UltrametricTriangle line 55
4. lemma OAI.SphericalPerceptron.gg_ultrametric_triangle line 58
5. lemma OAI.SphericalPerceptron.scalarArray_ultrametric_triangle line 75
6. lemma OAI.SphericalPerceptron.ultrametric_triangle_small_eq line 95
7. lemma OAI.SphericalPerceptron.ultrametric_sum_no_crossing line 105
8. theorem OAI.SphericalPerceptron.joint_gg_no_crossing line 121
9. theorem OAI.SphericalPerceptron.joint_gg_crossed_regions_null line 150