OAI/Probability/Perceptron/Variational/FiniteFieldModel.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.integral_finite_label line 11
2. structure OAI.SphericalPerceptronFreeEnergy.FiniteFieldModel line 26
3. def OAI.SphericalPerceptronFreeEnergy.FiniteFieldModel.weight line 35
4. lemma OAI.SphericalPerceptronFreeEnergy.FiniteFieldModel.weight_pos line 38
5. lemma OAI.SphericalPerceptronFreeEnergy.FiniteFieldModel.weight_sum line 41
6. lemma OAI.SphericalPerceptronFreeEnergy.FiniteFieldModel.integral line 45
7. def OAI.SphericalPerceptronFreeEnergy.FiniteFieldModel.coupling line 53
8. lemma OAI.SphericalPerceptronFreeEnergy.FiniteFieldModel.coupling_nonneg line 57
9. lemma OAI.SphericalPerceptronFreeEnergy.FiniteFieldModel.coupling_fst line 60
10. lemma OAI.SphericalPerceptronFreeEnergy.FiniteFieldModel.coupling_snd line 71
11. lemma OAI.SphericalPerceptronFreeEnergy.FiniteFieldModel.coupling_cost line 81
12. lemma OAI.SphericalPerceptronFreeEnergy.FiniteFieldModel.values_mem line 90
13. def OAI.SphericalPerceptronFreeEnergy.FiniteFieldModel.pressure line 109
14. lemma OAI.SphericalPerceptronFreeEnergy.FiniteFieldModel.pressure_bound line 112
15. theorem OAI.SphericalPerceptronFreeEnergy.exists_finiteFieldModel line 122