OAI/Probability/Perceptron/Variational/GlobalContactLimit.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.compactPositivePairLaw_field_integral line 15
2. lemma OAI.SphericalPerceptronFreeEnergy.compactPositivePairLaw_field_quantile line 35
3. theorem OAI.SphericalPerceptronFreeEnergy.source_global_contact_limit_field line 66
4. theorem OAI.SphericalPerceptronFreeEnergy.source_global_contact_limit_quantile_field line 83
5. lemma OAI.SphericalPerceptronFreeEnergy.sourceLabelLaw_ae line 107
6. def OAI.SphericalPerceptronFreeEnergy.sourceThresholdDirection line 113
7. lemma OAI.SphericalPerceptronFreeEnergy.sourceThresholdDirection_nonneg line 116
8. lemma OAI.SphericalPerceptronFreeEnergy.sourceThresholdDirection_le_one line 119
9. lemma OAI.SphericalPerceptronFreeEnergy.sourceThresholdDirection_monotone line 122
10. lemma OAI.SphericalPerceptronFreeEnergy.sourceThresholdDirection_stoploss line 129
11. lemma OAI.SphericalPerceptronFreeEnergy.stoploss_integrable line 140
12. lemma OAI.SphericalPerceptronFreeEnergy.source_field_stoploss line 145