OAI/Probability/SphericalField/Fields/FiniteModels.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptron.integral_finite_label line 13
2. lemma OAI.SphericalPerceptron.FiniteFieldModel.weight_pos line 28
3. lemma OAI.SphericalPerceptron.FiniteFieldModel.weight_sum line 31
4. lemma OAI.SphericalPerceptron.FiniteFieldModel.integral line 35
5. def OAI.SphericalPerceptron.FiniteFieldModel.coupling line 43
6. lemma OAI.SphericalPerceptron.FiniteFieldModel.coupling_nonneg line 47
7. lemma OAI.SphericalPerceptron.FiniteFieldModel.coupling_fst line 50
8. lemma OAI.SphericalPerceptron.FiniteFieldModel.coupling_snd line 61
9. lemma OAI.SphericalPerceptron.FiniteFieldModel.coupling_cost line 71
10. lemma OAI.SphericalPerceptron.FiniteFieldModel.values_mem line 80
11. lemma OAI.SphericalPerceptron.FiniteFieldModel.pressure_bound line 99