OAI/Probability/Perceptron/Variational/GlobalContact.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptronFreeEnergy.sourceStepFieldCap line 13
2. def OAI.SphericalPerceptronFreeEnergy.sourceContactCompactDomain line 16
3. lemma OAI.SphericalPerceptronFreeEnergy.sourceStepFieldCap_compact line 19
4. lemma OAI.SphericalPerceptronFreeEnergy.sourceContactCompactDomain_compact line 22
5. lemma OAI.SphericalPerceptronFreeEnergy.sourceContactCompactDomain_nonempty line 26
6. lemma OAI.SphericalPerceptronFreeEnergy.sourceContactCompactDomain_subset line 33
7. def OAI.SphericalPerceptronFreeEnergy.sourceStepContactObjective line 38
8. lemma OAI.SphericalPerceptronFreeEnergy.sourceStepContactObjective_continuousOn line 47
9. lemma OAI.SphericalPerceptronFreeEnergy.source_global_contact_exists line 66
10. lemma OAI.SphericalPerceptronFreeEnergy.source_global_contact_perturbation_min line 76
11. lemma OAI.SphericalPerceptronFreeEnergy.source_global_contact_field line 103