OAI/Probability/Perceptron/Variational/QuantileLimit.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.scalarArray_nonnegative line 12
2. lemma OAI.SphericalPerceptronFreeEnergy.compact_spin_nonnegative line 35
3. def OAI.SphericalPerceptronFreeEnergy.compactPositivePair line 45
4. lemma OAI.SphericalPerceptronFreeEnergy.compactPositivePair_measurable line 48
5. def OAI.SphericalPerceptronFreeEnergy.compactPositivePairLaw line 52
6. instance OAI.SphericalPerceptronFreeEnergy.compactPositivePairLaw_probability line 55
7. lemma OAI.SphericalPerceptronFreeEnergy.compactPositivePairLaw_no_crossing line 59
8. lemma OAI.SphericalPerceptronFreeEnergy.compactPositivePairLaw_quantile line 87
9. lemma OAI.SphericalPerceptronFreeEnergy.compactPositivePairLaw_label line 96
10. theorem OAI.SphericalPerceptronFreeEnergy.source_contact_limit_quantile line 124